Document Open Access Logo

Three Roads to de Finetti’s Theorem in Lean 4 (Short Paper)

Author Cameron Freer

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.34.pdf
  • Filesize: 0.7 MB
  • 9 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • exchangeability
  • de Finetti’s theorem
  • Lean 4
  • formalized mathematics
  • AI-assisted formalization

Metrics

Abstract

We present a Lean 4 formalization of the de Finetti–Ryll-Nardzewski theorem for infinite sequences of random variables on standard Borel spaces, establishing that every exchangeable sequence is conditionally i.i.d. The development closely follows Kallenberg’s modern treatment of probabilistic symmetries and formalizes three distinct proofs of the key implication, with the second and third formalized for real-valued square-integrable sequences: (i) a reverse‑martingale argument due to Aldous, (ii) an elementary L² approach based on contractability bounds and Cesàro convergence, and (iii) an ergodic‑theoretic proof via the Koopman operator and the mean ergodic theorem. The library contains over 42,000 lines of code and was completed in three months with extensive use of Claude and GPT models, together with a reusable Lean proof-engineering skill for agentic coding systems developed during the project. The three proofs share a uniform common ending, so each route had to produce the same finite conditional-factorization interface before the final conclusion. This provided a cross-check on these independent routes during AI-assisted development.

Cite As Get BibTex

Cameron Freer. Three Roads to de Finetti’s Theorem in Lean 4 (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 34:1-34:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.34

Author Details

Cameron Freer
  • Massachusetts Institute of Technology, Cambridge, MA, USA

Acknowledgements

The author thanks Daniel M. Roy for suggesting this project and for advice throughout; and Mauricio Barba, Fabian Zaiser, Katherine Collins, McCoy Becker, Jason Rute, and Rémy Degenne for helpful conversations or feedback on drafts. Thanks also to users of the skill who have contributed bug fixes or feature implementations, and to the anonymous reviewers for comments that improved the paper and the formalization.

Supplementary Materials

References

  1. David J. Aldous. Exchangeability and related topics. In Ecole d'Ete de Probabilites de Saint-Flour XIII - 1983, volume 1117 of Lecture Notes in Mathematics, pages 1-198. Springer, 1985. URL: https://doi.org/10.1007/BFb0099421.
  2. Bruno de Finetti. Funzione caratteristica di un fenomeno aleatorio. Atti della Reale Accademia Nazionale dei Lincei, Serie VI, Memorie, 4(5):86-133, 1930. URL: http://www.brunodefinetti.it/Opere/funzioneCaratteristica.pdf.
  3. Bruno de Finetti. La prévision: ses lois logiques, ses sources subjectives. Annales de l'Institut Henri Poincaré, 7(1):1-68, 1937. URL: https://eudml.org/doc/79004.
  4. Rémy Degenne, David Ledvinka, Etienne Marion, and Peter Pfaffelhuber. Formalization of Brownian motion in Lean, 2025. URL: https://doi.org/10.48550/arXiv.2511.20118.
  5. Oliver Dressler. Lean Theorem Prover MCP. GitHub repository, 2025. URL: https://github.com/oOo0oOo/lean-lsp-mcp.
  6. Cameron Freer. lean4-skills: Lean 4 coding-assistant skill for Claude Code. GitHub repository, 2025. URL: https://github.com/cameronfreer/lean4-skills.
  7. Cameron Freer. exchangeability: Exchangeability and de Finetti’s theorem in Lean 4, v1.2. GitHub repository, 2026. URL: https://github.com/cameronfreer/exchangeability.
  8. Edwin Hewitt and Leonard J. Savage. Symmetric measures on Cartesian products. Transactions of the American Mathematical Society, 80(2):470-501, 1955. URL: https://doi.org/10.1090/S0002-9947-1955-0076206-8.
  9. Thomas Hubert, Rishi Mehta, Laurent Sartran, et al. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, 651:607-613, 2026. URL: https://doi.org/10.1038/s41586-025-09833-y.
  10. Olav Kallenberg. Probabilistic Symmetries and Invariance Principles. Probability and Its Applications. Springer, 2005. URL: https://doi.org/10.1007/0-387-28861-9.
  11. Andrei Kozyrev, Gleb Solovev, Nikita Khramov, and Anton Podkopaev. CoqPilot, a plugin for LLM-based generation of proofs. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024), 2024. URL: https://doi.org/10.1145/3691620.3695357.
  12. Junqi Liu, Zihao Zhou, Zekai Zhu, Marco Dos Santos, Weikun He, Jiawei Liu, Ran Wang, Yunzhou Xie, Junqiao Zhao, Qiufeng Wang, Lihong Zhi, Jia Li, and Wenda Li. Numina-Lean-Agent: An open and general agentic reasoning system for formal mathematics. arXiv preprint, 2026. URL: https://doi.org/10.48550/arXiv.2601.14027.
  13. Azim Ospanov, Farzan Farnia, and Roozbeh Mohit. APOLLO: Automated LLM and Lean collaboration for advanced formal reasoning. In Advances in Neural Information Processing Systems 38 (NeurIPS 2025), 2025. URL: https://proceedings.neurips.cc/paper_files/paper/2025/hash/3b77109ad4dd4ba82d07cacd4b24207e-Abstract-Conference.html.
  14. Czesław Ryll-Nardzewski. On stationary sequences of random variables and the de Finetti’s equivalence. Colloquium Mathematicum, 4(2):149-156, 1957. URL: https://doi.org/10.4064/cm-4-2-149-156.
  15. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Lean Copilot: Large language models as copilots for theorem proving in lean. In George Pappas, Pradeep Ravikumar, and Sanjit A. Seshia, editors, Proceedings of the International Conference on Neuro-symbolic Systems, volume 288 of Proceedings of Machine Learning Research, pages 144-169. PMLR, 2025. URL: https://proceedings.mlr.press/v288/song25a.html.
  16. Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An in-context learning agent for formal theorem-proving. In Conference on Language Modeling (COLM), 2024. URL: https://openreview.net/forum?id=V7HRrxXUhN.
  17. Sean Welleck and Rahul Saha. LLMSTEP: LLM proofstep suggestions in Lean. arXiv preprint, 2023. URL: https://doi.org/10.48550/arXiv.2310.18457.
  18. Yichen Xu and Martin Odersky. Agentic proof automation: A case study. arXiv preprint, 2026. URL: https://doi.org/10.48550/arXiv.2601.03768.
  19. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. In Advances in Neural Information Processing Systems 36 (NeurIPS 2023), 2023. URL: https://proceedings.neurips.cc/paper_files/paper/2023/hash/4441469427094f8873d0fecb0c4e1cee-Abstract-Datasets_and_Benchmarks.html.
  20. Kexing Ying and Rémy Degenne. A formalization of Doob’s martingale convergence theorems in mathlib. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023), 2023. URL: https://doi.org/10.1145/3573105.3575675.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact