Interactive Theorem Provers (or Proof Assistants) are tools that verify and partially automate mathematical proofs. The process of encoding mathematics into these systems, known as formalisation, has gained significant interest due to its role in proof verification, generating verified code for computer algebra systems, and expanding digital mathematical libraries. It seems likely with the growth in sophistication of proof assistants, and progress of Generative AI technologies, interactive theorem provers will become a useful aide for research and teaching of mathematics. Lean, a leading proof assistant, has grown in popularity thanks to its extensive mathlib library, which now covers most undergraduate mathematics and beyond. Notable milestones include the Liquid Tensor Experiment, which formalised a key result by Fields medalist Peter Scholze, and the rapid formalisation of the Polynomial Freiman-Ruzsa Conjecture led by Terry Tao.The goal of the workshop is to introduce mathematicia...
Description