Big proof
Created: | 2017-07-19 17:02 |
---|---|
Institution: | Isaac Newton Institute for Mathematical Sciences |
Description: | Proofs as constructive demonstrations of mathematical validity have been at the heart of mathematics since antiquity. Formal proof systems capture the definitions, statements, and proofs of mathematical discourse using precisely defined formal languages and rules of inference. Formal proofs have enabled mathematicians to rigorously explore foundational issues of expressiveness, consistency, independence, completeness, computability, and decidability. The formalisation of proof facilitates the representation and manipulation of mathematical knowledge with modern digital computers. During the last sixty years, the digitisation of formal mathematics has yielded satisfiability solvers, rewriting engines, computer algebra systems, automated theorem provers, and interactive proof assistants. Proof technology can be used to perform large calculations reliably, solve systems of constraints, discover and visualise examples and counterexamples, simplify expressions, explore hypotheses, navigate large libraries of mathematical knowledge, capture abstractions and patterns of reasoning, and interactively construct proofs. The scale and sophistication of proof technology is approaching a point where it can effectively aid human mathematical creativity at all levels of expertise. Modern satisfiability solvers can efficiently solve problems with millions of Boolean constraints in hundreds of thousands of variables. Automated theorem provers have discovered proofs of open problems. Interactive proof assistants have been used to check complicated mathematical proofs such as those for the Kepler’s conjecture and the Feit-Thompson odd order theorem. Such systems have also been applied to the verification of practical artifacts such as central processing units (CPUs), compilers, operating system kernels, file systems, and air traffic control systems. Several high-level programming languages employ logical inference as a basic computation step.
This programme is directed at the challenges of bringing proof technology into mainstream mathematical practice. The specific challenges addressed include Novel pragmatic foundations for representing mathematical knowledge and vernacular inspired by set theory, category theory, and type theory. Large-scale formal mathematical libraries that capture background knowledge spanning a range of domains. Algorithmic and engineering issues in building and integrating large-scale inference engines. The social exploration and curation of formalised mathematical and scientific knowledge. Educational proof technology in support of collaborative learning. This programme brings together mathematicians interested in employing proof technology in their research, logicians exploring pragmatic and foundational issues in the formalisation of mathematics, and computer scientists engaged in developing and applying proof technology. The programme includes a week-long workshop exploring foundational, theoretical, and practical challenges in exploiting proof technology to transform mathematical practice across a range of scientific and engineering disciplines. A key expected output is a concrete, long-term research agenda for making computational inference a basic technology for formalising, creating, curating, and disseminating mathematical knowledge in digital form. |
Media items
This collection contains 70 media items.
Media items
Automated theorem proving in first-order logic: from superposition to instantiation
Korovin, K
Thursday 27th July 2017 - 13:30 to 14:30
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Fri 25 Aug 2017
Categorical structures for type theory in univalent foundations"
Ahrens , B
Thursday 27th July 2017 - 16:30 to 17:30
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Fri 28 Jul 2017
A MathComp Library tour
Gonthier, G
Friday 28th July 2017 - 11:00 to 12:00
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Fri 25 Aug 2017
A simple prover in the browser
Ayers, E
Monday 17th July 2017 - 17:00 to 17:30
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Wed 26 Jul 2017
A tutorial introduction to Agda
Abel, A
Friday 30th June 2017 - 11:00 to 12:00
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Fri 21 Jul 2017
A tutorial introduction to the PVS proof assistant
Shankar, N
Friday 30th June 2017 - 10:00 to 11:00
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Fri 21 Jul 2017
A Verified ODE Solver and Smale's 14th Problem
Immler, F
Thursday 6th July 2017 - 13:40 to 14:20
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Mon 24 Jul 2017
Accessible Reasoning with Diagrams: Ontology Debugging
Jamnik, M
Thursday 13th July 2017 - 14:30 to 15:30
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Wed 26 Jul 2017
After Math: Reasoning, Computing, and Proof in the Postwar United States (via Skype)
Dick, S
Friday 14th July 2017 - 13:30 to 14:30
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Wed 26 Jul 2017
An Industrially Useful Prover
Moore, J
Friday 7th July 2017 - 13:30 to 14:30
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Mon 24 Jul 2017
An overview of the Flyspeck project
Hales, T
Wednesday 26th July 2017 - 14:30 to 15:30
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Fri 25 Aug 2017
Auto2 prover in Isabelle
Zhan, B
Monday 17th July 2017 - 16:30 to 17:00
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Wed 26 Jul 2017
Big Conjectures
Hales, T
Monday 10th July 2017 - 10:00 to 11:00
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Mon 24 Jul 2017
Big Proof & Education
Avigad, J
Monday 24th July 2017 - 15:30 to 17:30
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Fri 25 Aug 2017
Building blocks towards modeling the physical world: analysis, geometry, computer arithmetics
Bertot, Y
Tuesday 25th July 2017 - 11:00 to 12:00
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Fri 25 Aug 2017
CDSAT: conflict-driven theory combination
Bonacina, M
Monday 17th July 2017 - 11:00 to 12:00
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Fri 25 Aug 2017
Classical Analysis in Lean & Isabelle
Hölzl, J
Tuesday 4th July 2017 - 13:00 to 14:00
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Fri 21 Jul 2017
Combining Machine Learning and Automated Reasoning: Some Training Examples
Urban, J
Tuesday 18th July 2017 - 13:30 to 14:30
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Wed 26 Jul 2017
Computer Algebra and Formal Proof
Davenport, J
Friday 21st July 2017 - 11:00 to 12:00
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Fri 25 Aug 2017
Concise - a synthesis of types, grammars, semantics
Neumaier, A
Wednesday 26th July 2017 - 11:00 to 12:00
Collection: Big proof
Institution: Isaac Newton Institute for Mathematical Sciences
Created: Fri 25 Aug 2017