# 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 71 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