Episode 207 - GluuFederation/identerati-office-hours GitHub Wiki
Title: Book Club: The Proof in the Code
- Host: Mike Schwartz, Founder/CEO Gluu
- Guest: Rohit Khare, Identerati and legendary Product Manager
Channels
Description
Can a computer prove something is unquestionably true? In this episode, we discuss Kevin Hartnett’s The Proof in the Code and the rise of Lean from a Microsoft Research project to a powerful tool for mathematics and AI. We explore how formal proofs could transform human–computer collaboration, software assurance, and our understanding of truth.
Homework
- The Proof in the Code: How a Truth Machine Is Transforming Math and AI by Kevin Hartnett published by Quanta Books, available on Amazon
- Lean FRO
Lean in the Real World
- Amazon: Cedar, 2024
- Microsoft: Verifying Rust cryptography in SymCrypt, from standards to code
- Meta: Teaching AI advanced mathematical reasoning, 2022 e.g. Facebook Atlas
- Google AlphaProof: AI achieves silver-medal standard solving International Mathematical Olympiad problems
Rohit's links
- Leanstral: Open-Source foundation for trustworthy vibe-coding | Mistral AI
- Pramaana Labs - AI That Proves Its Work
- Math, Inc.
- Axiom
- Harmonic
- sflean.group @ Mox SF, 1680 Mission St (ask for the door code in Discord) | sflean
- Mathematics from Scratch with Lean Kick-off - Google Slides SFLean Mock Slides July 6 archive
- Sigil Logic
- Archway — Formal verification for AI agents in enterprise code
- Archway Labs Linkedin Page
- Jane Street Blog - Formal methods and the future of programming
- Lean 4 Web
- Future of Mathematics Symposium - Stanford University
Takeaways
-
⚡ Lean is moving from math research into production software engineering. AWS uses Lean to specify and prove Cedar’s security properties before testing the production Rust implementation against the formal model, while Microsoft uses Lean to verify Rust cryptography that ships in Windows.
-
⚡ Like winning a Chess or Go game, Lean validation gives AI an "automated reward source." Meta’s HTPS and Google DeepMind’s AlphaProof search through proof steps and use Lean to determine whether the result is actually correct, turning theorem proving into a reinforcement-learning environment rather than a plausibility contest.
-
⚡ Autoformalization may solve Lean’s biggest AI bottleneck: insufficient training data. DeepMind uses Gemini to translate informal problems into formal statements, while Meta’s ATLAS project is converting entire mathematics textbooks into a large, reusable Lean library—although the generated material still requires evaluation, curation and human review.
-
⚡ Lean leverages open source collaboration. Lean is better because of Mathlib, which no one person could produce.
-
⚡ Lean’s strategic importance is now clear. But its long-term economic model is not. Amazon, Microsoft, Meta and Google are deriving substantial value from Lean—but the core ecosystem still needs a durable foundation, maintenance organization and post-FRO funding commitment.