lean-forward.github.io - Lean Forward

Example domain paragraphs

Project funded by the Dutch Research Council (NWO) Vidi grant number 016.Vidi.189.037 from January 2019 to December 2023 Principal investigator: Jasmin Blanchette Host institution: Vrije Universiteit Amsterdam

Proof assistants (also called interactive theorem provers) are increasingly used in academia and industry to verify the correctness of hardware, software, and protocols. However, despite the trustworthiness guarantees they offer, most mathematicians find them too laborious to use. The goal of the Lean Forward project is to collaborate with number theorists to formally prove theorems about research mathematics and to address the main usability issues hampering the adoption of proof assistants in mathematical

Proof assistants (also called interactive theorem provers) are interactive tools that make it possible to develop computer-checked, formal proofs of theorems. Two early systems, Automath and Mizar, were designed to mechanize mathematics. Landmark achievements include the formal proofs of the Kepler conjecture by Hales et al. and of the odd-order theorem by Gonthier et al. The main strength of proof assistants is their trustworthiness: all definitions and lemmas are checked for well-formedness, and even the

Links to lean-forward.github.io (5)

leanprover-community.github.io Lean community
matryoshka-project.github.io Matryoshka: Fast Interactive Verification through Strong Higher-Order Automation
abentkamp.github.io Alexander Bentkamp
limperg.de Jannis Limperg
desharnais.me index