Explore the intersection of formal methods and pure mathematics through this comprehensive workshop featuring leading experts from both computer science and mathematics communities. Discover how interactive proof assistants, automated reasoning systems, computer algebra systems, and machine learning technologies are revolutionizing mathematical research and proof verification. Learn about cutting-edge developments in formal mathematics, including the Lean proof assistant, autoformalization with large language models, and deep learning applications in theorem proving. Examine real-world applications through case studies such as the Liquid Tensor Experiment, computer-assisted proofs in quadratic forms, and formalization of number theory concepts. Gain insights into practical tools and methodologies including SMT solvers, the UniMath library, univalent foundations, and various theorem provers like HolPy and Coq. Understand how reinforcement learning is being used to find counterexamples to mathematical conjectures and how machine learning assists in formulating new mathematical hypotheses. Engage with discussions on the challenges and future prospects of automated reasoning, symbolic computation verification, and the role of abstraction in formal mathematics, all presented by renowned researchers from institutions worldwide in this collaborative exploration of machine-assisted mathematical discovery.

Syllabus

Andrej Bauer - Formalizing invisible mathematics - IPAM at UCLA
Leonardo de Moura - The Lean proof assistant: introduction and challenges - IPAM at UCLA
Patrick Massot - Formal mathematics for mathematicians and mathematics students - IPAM at UCLA
Tony Wu - Autoformalization with Large Language Models - IPAM at UCLA
Geordie Williamson - What can the working mathematician expect from deep learning? - IPAM at UCLA
Jason Rute - Deep learning in interactive theorem proving - IPAM at UCLA
Adam Wagner - Finding counterexamples to conjectures via reinforcement learning - IPAM at UCLA
Heather Macbeth - Algorithm and abstraction in formal mathematics - IPAM at UCLA
John Harrison - Formalization and Automated Reasoning: A Personal and Historical Perspective
Marc Lackenby - Using machine learning to formulate mathematical conjectures - IPAM at UCLA
Adam Topaz - The Liquid Tensor Experiment - IPAM at UCLA
James Davenport - How to prove a calculation correct? - IPAM at UCLA
Anne Baanen - Computing with or despite the computer - IPAM at UCLA
Haniel Barbosa - Better SMT proofs for certifying compliance and correctness - IPAM at UCLA
Benedikt Ahrens - Univalent Foundations and the UniMath library - IPAM at UCLA
Johnathan Hanke - Computer-Assisted Proofs in the Arithmetic of Quadratic Forms - IPAM at UCLA
Bohua Zhan - Verifying symbolic computation in the HolPy theorem prover - IPAM at UCLA
Petra Hozzova - Automation of Induction in Saturation - IPAM at UCLA
Pascal Fontaine - SMT: quantifiers, and future prospects - IPAM at UCLA
Maria Ines de Frutos Fernandez - Formalizing Norm Extensions and Applications to Number Theory
Micaela Mayero - Overview of real numbers in theorem provers: application with real analysis in Coq