Scratch-like environment for Lean 4 is coming! This is another game level😉 for learning Lean 4 youtu.be/Um_2x5wHi20?t=3179 #LeanLang #LeanProver #Scratch #Play #Education #Proofs #Mathematics

This week, @QuantaBks released "The Proof in the Code" by journalist Kevin Hartnett, which tells the story of the birth and rise of Lean, a proof assistant that’s shifting the way mathematicians seek truth: bit.ly/43msryr #math #science

"AI may have the answers, but mathematics has the questions." With all the recent excitement around AI for math, many start to wonder: can mathematics be automated? And what does it mean to learn and understand math? For EP5, we're thrilled to talk with Prof. Jeremy Avigad, philosopher & mathematician @CarnegieMellon and one of the early forces behind 3w. This episode features rich technical discussions on AI & mathematics, as well as many touching moments where Jeremy shares his vision for the future of mathematicians, math education, and mathematics itself. Outline: 0:00 - Teaser 1:04 - Monologue 2:50 - The Historical Landscape of AI for Mathematics 7:28 - Formalization and Computer-Aided Proof 11:56 - The Birth of the Lean Project 21:21 - Lean Blueprint, Model Training with Lean, Using Lean in Agentic Systems 29:48 - Making AI Actually Useful for Mathematicians 32:46 - How AI is Changing Mathematics 36:29 - "It's Our Mathematics, and Us Doing Mathematics" 43:04 - The Verification Gap in Human-AI Collaboration 47:46 - The Future of Math Education 52:23 - Capital, Startups, and the Mathematicians' Ecosystem 1:01:08 - Predictions

Did you miss the panels marking the launch of The Proof in the Code, @KSHartnett's book on the development of Lean and Mathlib? Both conversations are now up to watch. The Mathematicians, with Johan Commelin, Kevin Buzzard, and @AlexKontorovich . The Builders, with @leodemoura, Sebastian Ullrich (@derKha), and Jeremy Avigad. Watch both: youtube.com/playlist?list=PL… #LeanLang #LeanProver #FormalMathematics #SoftwareVerification

I've been telling people for 25 years that Jane Street is not interested in formal methods. No more! And we're actively hiring to form a new formal methods team!

Lean is software that allows mathematical proofs to be written and checked as computer code. Mathematician Terence Tao uses it as a part of his collaborative approach to solving complex mathematical problems. quantamagazine.org/how-terry…

Flying now to Jerusalem, to give a mini-workshop on Lean for Mathematicians @leanprover at the Einstein Institute @HebrewU. mathematics.huji.ac.il/event… (Unfortunately the workshop is oversubscribed already, with ~80 participants, so they're not taking more.)

In his new book, "The Proof in the Code: How a Truth Machine Is Transforming Math and AI," Kevin Hartnett (@KSHartnett) tells the definitive story of computer program Lean in an effort to answer a longstanding question: Can computers reveal universal truths? Out today from @QuantaBks: bit.ly/43X5To1 #science #math

To simultaneously prove a theorem while formalizing it a link is needed between definitions, lemmas, propositions, theorems etc. in latex with corresponding declarations in lean. To do this I created a tool called span: github.com/pachterlab/span 2/

Terry Tao has become the foremost proponent of AI and Lean for math research. Today, @QuantaMagazine is running an excerpt from my book, "The Proof in the Code," about a project where Tao made the leap into this new way of working—his unconventional 2024 'equational theories' effort to map relationships between arithmetic laws.

Software like Lean, which allows mathematical proofs to be written and checked as computer code, could usher in a new, more collaborative era of problem solving. One of its most prominent supporters is mathematician Terence Tao. quantamagazine.org/how-terry…

SAIR Playground for the Modular Arithmetic Challenge: playground.sair.foundation/p…

The 2nd SAIR Competition is now open: the Modular Arithmetic Challenge. Can a neural network learn to compute (a × b) mod p for large numbers? Easy for standard algorithms, but a hard test of whether neural networks can generalize the computation. Join the SAIR competition: competition.sair.foundation/…

The Proof in the Code, @KSHartnett 's new book on the development of Lean and Mathlib, is out today. quantabooks.org/books/the-pr… To mark the launch, a two-part online panel series with the author, both 5pm UTC: The Mathematicians, June 11, with Johan Commelin, Kevin Buzzard, and Alex Kontorovich. Register: forms.gle/w16jkmsMqB2gF8t77 The Builders, June 12, with Leo de Moura, Sebastian Ullrich, and Jeremy Avigad. Register: forms.gle/PsxPkq3x2pESXQNKA

The second of two panels for the launch of The Proof in the Code, Kevin Hartnett's (@KSHartnett) new book on the development of Lean and Mathlib. The Builders. Friday, June 12, 5pm UTC. Joining Kevin Hartnett: Leo de Moura (@leodemoura), creator of Lean, co-founder and Chief Architect at the Lean FRO Sebastian Ullrich (@derKha), co-founder and Head of Engineering at the Lean FRO Jeremy Avigad, Professor of Philosophy and Mathematical Sciences at Carnegie Mellon University, Director of the Hoskinson Center for Formal Mathematics, and Directory of the Institute for Computer-Aided Reasoning in Mathematics They talk about Lean from the inside: its origins, its design, and where it's headed, and the long road from a research project to a system now used across mathematics and AI. Register: forms.gle/PsxPkq3x2pESXQNKA

Read more about Lean in Kevin Hartnett’s THE PROOF IN THE CODE, publishing June 9: quantabooks.org/books/the-pr…

A two-part online panel series marks the launch of The Proof in the Code, @KSHartnett 's new book on the development of Lean and Mathlib. Registration links below. The Mathematicians. Thursday, June 11, 5pm UTC. Johan Commelin, Kevin Buzzard, and Alex Kontorovich join Kevin Hartnett to discuss what it means to formalize mathematics in Lean, and how computer verification is changing the way mathematicians collaborate, build trust, and decide what counts as proof. The Builders. Friday, June 12, 5pm UTC. Leo de Moura, Sebastian Ullrich, and Jeremy Avigad join Kevin Hartnett to talk about Lean from the inside: its origins, its design, and the road from a research project to a system now used across mathematics and AI. The Mathematicians: forms.gle/w16jkmsMqB2gF8t77 The Builders: forms.gle/PsxPkq3x2pESXQNKA

Mathematically, Aumann’s theorem means I have to agree to agree with Scott! 🤝 Happy to bring formal verification to economics. Catch our exclusive in @FortuneMagazine. @axiommathai @leanprover