La @socmathfrance.bsky.social a attribué le prix Demailly 2026 pour la science ouverte en mathématiques à Mathlib, un projet exemplaire en matière d’ouverture et d’organisation collaborative.
lnkd.in/eXzPxe9A
@marind.eurosky.social
lnkd.in/eXzPxe9A
@marind.eurosky.social
Le prix Demailly 2026, pour la sciences ouverte en mathématiques, est attribué au projet
Mathlib
leanprover-community.github.io/mathlib-over...
Félicitations !
Un prix SMF, SMAI, SFdS et EPIGA
Plus d'infos : epiga.episciences.org/page/session...
Mathlib
leanprover-community.github.io/mathlib-over...
Félicitations !
Un prix SMF, SMAI, SFdS et EPIGA
Plus d'infos : epiga.episciences.org/page/session...
November 5, 2026 at 12:54 PM
La @socmathfrance.bsky.social a attribué le prix Demailly 2026 pour la science ouverte en mathématiques à Mathlib, un projet exemplaire en matière d’ouverture et d’organisation collaborative.
lnkd.in/eXzPxe9A
@marind.eurosky.social
lnkd.in/eXzPxe9A
@marind.eurosky.social
Aujourd'hui a lieu la remise du Prix Demailly 2026 pour la science ouverte en mathématiques, attribué au projet Mathlib. Félicitations !
Le prix sera remis cet après-midi lors d'une cérémonie au CIRM qui sera également retransmise en ligne.
Plus d'infos :
epiga.episciences.org/page/session...
Le prix sera remis cet après-midi lors d'une cérémonie au CIRM qui sera également retransmise en ligne.
Plus d'infos :
epiga.episciences.org/page/session...
November 4, 2026 at 9:04 AM
Aujourd'hui a lieu la remise du Prix Demailly 2026 pour la science ouverte en mathématiques, attribué au projet Mathlib. Félicitations !
Le prix sera remis cet après-midi lors d'une cérémonie au CIRM qui sera également retransmise en ligne.
Plus d'infos :
epiga.episciences.org/page/session...
Le prix sera remis cet après-midi lors d'une cérémonie au CIRM qui sera également retransmise en ligne.
Plus d'infos :
epiga.episciences.org/page/session...
Lean 4 meets quantum physics: a 2D eigenspace in an Ammann–Beenker quasicrystal model:
substack.com/@odassoa/not...
#Lean4 #LeanProver #FormalMethods #Mathlib #QuantumPhysics #QuantumComputing #SpectralTheory #Quasicrystals #MathPhysics
substack.com/@odassoa/not...
#Lean4 #LeanProver #FormalMethods #Mathlib #QuantumPhysics #QuantumComputing #SpectralTheory #Quasicrystals #MathPhysics
Alessandro Odasso (@odassoa)
I am neither a mathematician nor a physicist but I am fascinated by LLMs becoming increasingly capable in science.
In the course of some conversations with GPT6 Astra series models, a potentially int...
substack.com
November 7, 2026 at 6:00 PM
Lean 4 meets quantum physics: a 2D eigenspace in an Ammann–Beenker quasicrystal model:
substack.com/@odassoa/not...
#Lean4 #LeanProver #FormalMethods #Mathlib #QuantumPhysics #QuantumComputing #SpectralTheory #Quasicrystals #MathPhysics
substack.com/@odassoa/not...
#Lean4 #LeanProver #FormalMethods #Mathlib #QuantumPhysics #QuantumComputing #SpectralTheory #Quasicrystals #MathPhysics
Here @Vierkantor
, @riccardobrasca.bsky.social @anatolededecker and Bhavik Mehta present on behalf of Mathlib winning the 2026 Jean-Pierre Demailly prize for open science in mathematics.
https://www.youtube.com/live/EMOvwgS5uzU?si=hHZw1hocv_-Ax4CV&t=324
(presentation proper starts at 14:18)
, @riccardobrasca.bsky.social @anatolededecker and Bhavik Mehta present on behalf of Mathlib winning the 2026 Jean-Pierre Demailly prize for open science in mathematics.
https://www.youtube.com/live/EMOvwgS5uzU?si=hHZw1hocv_-Ax4CV&t=324
(presentation proper starts at 14:18)
November 5, 2026 at 11:27 AM
Here @Vierkantor
, @riccardobrasca.bsky.social @anatolededecker and Bhavik Mehta present on behalf of Mathlib winning the 2026 Jean-Pierre Demailly prize for open science in mathematics.
https://www.youtube.com/live/EMOvwgS5uzU?si=hHZw1hocv_-Ax4CV&t=324
(presentation proper starts at 14:18)
, @riccardobrasca.bsky.social @anatolededecker and Bhavik Mehta present on behalf of Mathlib winning the 2026 Jean-Pierre Demailly prize for open science in mathematics.
https://www.youtube.com/live/EMOvwgS5uzU?si=hHZw1hocv_-Ax4CV&t=324
(presentation proper starts at 14:18)
6/ That check is already moving. Human experts have read the proof and understood it, Aaronson writes, and a short exposition by researchers at MIT and Stanford is already out. You can read the paper and the proof in a browser; rebuilding it needs Lean 4.33.0 and Mathlib.
November 9, 2026 at 2:00 AM
6/ That check is already moving. Human experts have read the proof and understood it, Aaronson writes, and a short exposition by researchers at MIT and Stanford is already out. You can read the paper and the proof in a browser; rebuilding it needs Lean 4.33.0 and Mathlib.
... nicht erwartet, das noch zu seinen Lebzeiten zu erleben. Und das, obwohl er schon vor diesen jüngsten KI-Durchbrüchen mit dem Beweisassistenten Lean und der mathematischen Bibliothek Mathlib gearbeitet hatte. 3/25
November 5, 2026 at 6:23 PM
... nicht erwartet, das noch zu seinen Lebzeiten zu erleben. Und das, obwohl er schon vor diesen jüngsten KI-Durchbrüchen mit dem Beweisassistenten Lean und der mathematischen Bibliothek Mathlib gearbeitet hatte. 3/25
This. Filippo, in an ode to the mathlib community and the formalisation community in general (not just in Lean), also address the paradoxical pressures against understanding in the pursuit of prestige, i.e. the mathematical publishing industry.
Formalisation as a concrete manifestation of mathematical understanding https://proofsandprompts.com/2026/11/08/formalisation-as-a-concrete-manifestation-of-mathematical-understanding/
mathstodon.xyz
November 8, 2026 at 6:03 PM
This. Filippo, in an ode to the mathlib community and the formalisation community in general (not just in Lean), also address the paradoxical pressures against understanding in the pursuit of prestige, i.e. the mathematical publishing industry.
The ceremony for the 2026 Demailly prize, awarded to mathlib, will take place in a couple of hours. You can follow it live at youtube.com/live/EMOvwgS...
YouTube video
youtube.com
November 4, 2026 at 10:28 AM
The ceremony for the 2026 Demailly prize, awarded to mathlib, will take place in a couple of hours. You can follow it live at youtube.com/live/EMOvwgS...
つまり，Axomは自然言語の数学書をLeanのMathlibに繋げて形式検証できる仕組みがあるから，当然全分野の数学書についてやるよね．そしてそのLeanで形式化された知識をAIエージェントが縦横無尽に使いこなし，新しい数学が生まれてくることになると思う．なにより数学が工学の課題になっていくよね…
November 5, 2026 at 3:58 AM
つまり，Axomは自然言語の数学書をLeanのMathlibに繋げて形式検証できる仕組みがあるから，当然全分野の数学書についてやるよね．そしてそのLeanで形式化された知識をAIエージェントが縦横無尽に使いこなし，新しい数学が生まれてくることになると思う．なにより数学が工学の課題になっていくよね…
Tou parado na formalização pq meu pc tem nem espaço no HD pro tanto q o mathlib puxa. Mas mil low hanging fruits hein
November 2, 2026 at 6:50 PM
Tou parado na formalização pq meu pc tem nem espaço no HD pro tanto q o mathlib puxa. Mas mil low hanging fruits hein
The Stacks Project, formalized in Lean axiommath.ai/research/the... AxomのStacks ProjectをLean形式化したこれ，一部の数学者以外静かだけど，彼らは自然言語からLeanへの翻訳器だけでなくて，形式化した命題を形式検証し，必要な補題を生成し、既存のMathlibと統合するシステムを持ってるのね…
November 5, 2026 at 3:58 AM
The Stacks Project, formalized in Lean axiommath.ai/research/the... AxomのStacks ProjectをLean形式化したこれ，一部の数学者以外静かだけど，彼らは自然言語からLeanへの翻訳器だけでなくて，形式化した命題を形式検証し，必要な補題を生成し、既存のMathlibと統合するシステムを持ってるのね…
Projects like Wikipedia and Mathlib are very important, and I don't see why we just leave them solely to volunteers and outside orgs rather than also academia!
October 28, 2026 at 3:15 PM
Projects like Wikipedia and Mathlib are very important, and I don't see why we just leave them solely to volunteers and outside orgs rather than also academia!
I agree that Wikipedia & Mathlib are very good. For that to continue, they need stability.
Conversely Linux & Debian are very good. They are no longer stable because of a change in contributors. This is not bringing improvement but fear and a drop in volunteering quality.
(Universities were good.)
Conversely Linux & Debian are very good. They are no longer stable because of a change in contributors. This is not bringing improvement but fear and a drop in volunteering quality.
(Universities were good.)
October 30, 2026 at 3:04 PM
I agree that Wikipedia & Mathlib are very good. For that to continue, they need stability.
Conversely Linux & Debian are very good. They are no longer stable because of a change in contributors. This is not bringing improvement but fear and a drop in volunteering quality.
(Universities were good.)
Conversely Linux & Debian are very good. They are no longer stable because of a change in contributors. This is not bringing improvement but fear and a drop in volunteering quality.
(Universities were good.)
Lean creator Leo de Moura tells Ben Lorica that while Mathlib took a decade to reach 2.5 million lines, AI is now generating 50-million-line Lean proofs. As code generation gets cheaper, machine-checked specifications matter more than traditional test suites.
AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura
Leo de Moura on Formal Proofs, AI Agents, and the End of “Trust Me” Code. Subscribe: Apple • Spotify • … More
thedataexchange.media
November 1, 2026 at 2:30 PM
Lean creator Leo de Moura tells Ben Lorica that while Mathlib took a decade to reach 2.5 million lines, AI is now generating 50-million-line Lean proofs. As code generation gets cheaper, machine-checked specifications matter more than traditional test suites.
what happens here is the opposite of the mass vibe-slinging that openai & friends are doing
TC builds foundations, harmonizes with upstream (mathlib) and sibling projects
TC builds foundations, harmonizes with upstream (mathlib) and sibling projects
October 27, 2026 at 5:45 AM
what happens here is the opposite of the mass vibe-slinging that openai & friends are doing
TC builds foundations, harmonizes with upstream (mathlib) and sibling projects
TC builds foundations, harmonizes with upstream (mathlib) and sibling projects
The Irrationality of ζ(5)
by Alex Hyman
We formalise the proof that is irrational from A. Fauzans 2026 preprint (Zenodo, doi:10.5281/zenodo.22826419), following the Lean 4/Mathlib formalisation of the same argument by domino14 (github.com/domino14/zeta5), of which this entry is a port.
by Alex Hyman
We formalise the proof that is irrational from A. Fauzans 2026 preprint (Zenodo, doi:10.5281/zenodo.22826419), following the Lean 4/Mathlib formalisation of the same argument by domino14 (github.com/domino14/zeta5), of which this entry is a port.
GitHub - domino14/zeta5
Contribute to domino14/zeta5 development by creating an account on GitHub.
github.com
October 29, 2026 at 4:45 PM
The Irrationality of ζ(5)
by Alex Hyman
We formalise the proof that is irrational from A. Fauzans 2026 preprint (Zenodo, doi:10.5281/zenodo.22826419), following the Lean 4/Mathlib formalisation of the same argument by domino14 (github.com/domino14/zeta5), of which this entry is a port.
by Alex Hyman
We formalise the proof that is irrational from A. Fauzans 2026 preprint (Zenodo, doi:10.5281/zenodo.22826419), following the Lean 4/Mathlib formalisation of the same argument by domino14 (github.com/domino14/zeta5), of which this entry is a port.
The full thing is 43.1 million lines of code, about 20 times the size of the entirety of Lean's mathlib, and more than triple the Fermat formalisation from a few weeks ago.
October 28, 2026 at 12:41 PM
The full thing is 43.1 million lines of code, about 20 times the size of the entirety of Lean's mathlib, and more than triple the Fermat formalisation from a few weeks ago.
I tried this again 6 months later. Claude Code got *way* farther this time (though I did use Opus 5.x):
github.com/vhxs/simplic...
I have the simplicial approximation theorem. The definitions are compatible with already exists in Mathlib. It took shockingly little input from me...
github.com/vhxs/simplic...
I have the simplicial approximation theorem. The definitions are compatible with already exists in Mathlib. It took shockingly little input from me...
October 27, 2026 at 1:53 AM
I tried this again 6 months later. Claude Code got *way* farther this time (though I did use Opus 5.x):
github.com/vhxs/simplic...
I have the simplicial approximation theorem. The definitions are compatible with already exists in Mathlib. It took shockingly little input from me...
github.com/vhxs/simplic...
I have the simplicial approximation theorem. The definitions are compatible with already exists in Mathlib. It took shockingly little input from me...
in searching, I also came across this odd website/project: taucetiproject.org
In CC's words: "a Lean library downstream of Mathlib where AI agents implement against human-written roadmaps."
In CC's words: "a Lean library downstream of Mathlib where AI agents implement against human-written roadmaps."
Tau Ceti — Tau Ceti
taucetiproject.org
October 27, 2026 at 1:53 AM
in searching, I also came across this odd website/project: taucetiproject.org
In CC's words: "a Lean library downstream of Mathlib where AI agents implement against human-written roadmaps."
In CC's words: "a Lean library downstream of Mathlib where AI agents implement against human-written roadmaps."
building on mathlib instead of next to it is the boring choice that ages well. a proof that agrees with upstream beats a viral claim nobody can check
October 27, 2026 at 7:25 AM
building on mathlib instead of next to it is the boring choice that ages well. a proof that agrees with upstream beats a viral claim nobody can check
It doesn't look like any of this is in Mathlib (yet anyways). I used CC to look for other existing Lean proofs out on the internet; didn't find much.
October 27, 2026 at 1:53 AM
It doesn't look like any of this is in Mathlib (yet anyways). I used CC to look for other existing Lean proofs out on the internet; didn't find much.
I'm also convinced this is the future of software engineering. I've built github.com/yamafaktory/..., a Lean 4 proof service that lets coding agents verify properties of the code they write. I think this kind of feedback loop will become a standard part of agentic development.
GitHub - yamafaktory/formal: A Lean 4 + Mathlib proof service for the agent working on your code
A Lean 4 + Mathlib proof service for the agent working on your code - yamafaktory/formal
github.com
October 25, 2026 at 7:23 AM
I'm also convinced this is the future of software engineering. I've built github.com/yamafaktory/..., a Lean 4 proof service that lets coding agents verify properties of the code they write. I think this kind of feedback loop will become a standard part of agentic development.
