"Mathlib has reached 2 million lines of code as of October 28. Thanks to everyone that contributed to Mathlib during the roughly 8 years of Mathlib's existence!"

https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/2.20million/near/553410451

#leanprover #mathlib

Readings shared October 8, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/09-readings_shared_10-08-25 #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Mathlib

Growing Mathlib: Maintenance of a large scale mathematical library. ~ Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Michael Rothgang, Damiano Testa. https://arxiv.org/abs/2508.21593 #ITP #LeanProver #Mathlib #Math

Readings shared October 3, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/04-readings_shared_10-03-25 #AI #ATP #AlphaProof #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Mathlib

Kevin Buzzard and Alex Kontorovich on the future of formal mathematics: A Mathlib initiative interview. ~ Oliver Nash. https://www.renaissancephilanthropy.org/news-and-insights/kevin-buzzard-and-alex-kontorovich-on-the-future-of-formal-mathematics-a-mathlib-initiative-interview #ITP #LeanProver #Mathlib #Math

The Mathlib initiative (Building the digital foundation of mathematics). https://mathlib-initiative.org/ #ITP #LeanProver #Mathlib #Math

Yapay zeka, büyük veri setlerini analiz etmekten karmaşık simülasyonlar oluşturmaya kadar, hesaplamalı matematiğin ağır işlerini üstlenerek büyük bir güç haline geldi. Şu an itibarıyla, YZ genellikle kendisine verilen ispatları adım adım doğrulayabiliyor; ancak nihai kararı ve en yaratıcı kanıt yöntemlerinin keşfini hâlâ insan zekasına bırakıyor.
Peki ya bu denge değişirse?
#YapayZeka #Matematik #AlphaProof #Lean #mathlib #DeepMind #YaşamOyunu
https://youtu.be/ZERkY5kExjI
https://monologblg.com/matematik-sadece-insana-mi-ait/

Readings shared September 17, 2025. https://jaalonso.github.io/vestigium/posts/2025/09/18-readings_shared_09-17-25 #AI #Autoformalization #CAS #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Macaulay2 #Math #Mathlib #Physics #Rocq #SMT

Domain specific (Documentation for Mathlib). ~ John Talbot, Richard M. Hill. https://www.renaissancephilanthropy.org/domain-specific-documentation-for-mathlib-1 #ITP #LeanProver #Mathlib

Трактат о природе формального доказательства

Мы пытались закрыть пробелы в доказательстве в Lean 4. Но вместо решений получили 120 000 токенов объяснений и одно слово: sorry . Из этого вырос философский трактат о природе формальных доказательств. Читать трактат

https://habr.com/ru/articles/946566/

#mathlib #Lean_4 #sorry #Proof #гипотеза_римана #формальные_доказательства #sorry_solver #автоматизация_доказательств #философия_математики

Readings shared September 1, 2025. https://jaalonso.github.io/vestigium/posts/2025/09/02-readings_shared_09-01-25 #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Mathlib #RustLang

Growing Mathlib: maintenance of a large scale mathematical library. ~ Anne Baanen et als. https://arxiv.org/abs/2508.21593 #ITP #LeanProver #Mathlib

Readings shared July 19, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/20-readings_shared_07-19-25 #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #Math #Mathlib #Reasoning #Rocq

Lean Finder: Semantic search for Mathlib that understands user intents. ~ Jialin Lu et als. https://openreview.net/forum?id=5SF4fFRw7u #ITP #LeanProver #Mathlib

I've installed the mathlib docs, but it's not a copy of its online version. I got only warningsbut no errors, and references are disabled by default for some reason. Well, it's only an alternate if my ISP is having a bad connection day. #mathlib #docs #lean #nomxd #Tech-talk🐾

To run Mathlib, I had to install Elan. It installs whatever Lean version Mathlib (or some package) needs. Doing it without Elan is a pain (I've tried), so we begin removing our installation of Lean. #lean #mathlib #elan #lake #MV #新曲公開 #オリジナル曲 #newmusic #Tech-talk🐾

Readings shared May 10, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/10-readings_shared_05-10-25 #ITP #LeanProver #Math #Mathlib #Python

LeanExplore: a new Mathlib search engine that combines semantic search embeddings, AI-generated translations, and PageRank to give optimized search results. https://www.leanexplore.com/ #ITP #LeanProver #Mathlib

#mathlib has a fascinating set of counterexamples, which includes, for example, a disproof of the Aharoni–Korman conjecture: https://leanprover-community.github.io/mathlib4_docs/Counterexamples/AharoniKorman.html

when i'm in a #lean4 phase, i often think of (much, much more trivial) false statements, so i decided to just start proving that they were indeed false: https://g.pyrope.net/simple-counterexamples

the pace of additions will be somewhat rapid because the proofs are only a couple of lines at most. they're fun to think about, though—how would you prove that (haskell syntax) Monad m => m a -> a is inconsistent?

Readings shared April 2, 2025. https://jaalonso.github.io/vestigium/posts/2025/04/02-readings_shared_04-02-25 #FunctionalProgramming #HOL4 #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Mathlib #Prolog