Big proof

Big proof's image
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.

Note: some media items are not shown, because they are only visible to Raven users. To see these media items, you must log in.
Showing results 1-20 of 69    < Prev    1 2 3 4    Next >
  •  

Media items

Automated theorem proving in first-order logic: from superposition to instantiation

   26 views

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"

   20 views

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

   20 views

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

   25 views

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

   31 views

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

   22 views

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

   15 views

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

   24 views

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)

   21 views

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

   26 views

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

   41 views

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

   22 views

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

   618 views

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

   50 views

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

   22 views

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

   22 views

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

   24 views

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

   25 views

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

   38 views

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

   53 views

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


[Results 1-20 of 69]    < Prev    1 2 3 4    Next >