#mathlib — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #mathlib, aggregated by home.social.
-
Formalized in Lean4:
The map F : K³ → K³ has constant Jacobian −2 yet identifies three points. This is no accident of algebra: F is, definitionally, the proof is rfl, the map "binary cubic with a marked simple root ↦ forget the marking", for the family cT³ − 2T²U + bTU² − 2aU³.
So every fiber is the set of simple roots of one cubic. The Keller condition says the root you stand on is simple, a local fact. It cannot control how many simple roots the cubic has: 3 off the discriminant hypersurface, 1 on it, 0 on its singular curve (the triple roots), which is exactly the locus the image misses. All machine-checked now, including disc = −4W and "missed curve = singular locus of the discriminant".
My favorite part is arithmetic: over any field of char ≠ 2, a fiber can never have exactly two rational points, two roots force a third. Vieta, made constructive.
The Jacobian Conjecture failed because pointwise simplicity of roots doesn't count roots.
-
Com començar a desenvolupar en Lean4? – Blog of Joaquim Puig
https://web.mat.upc.edu/joaquim.puig/posts/apunts_lean4_1/ -
@yoginho Perhaps not exactly the kind of "controlled labels" you are looking for, but here are some recent developments I've seen:
* the developer/maintainer of #syncthing is using the label "ai-slop" when rejecting certain PRs: https://github.com/syncthing/syncthing/pulls?q=is%3Apr+is%3Aclosed+label%3Aai-slop
* #mathlib uses the less emotionally charged label "LLM-generated": https://github.com/leanprover-community/mathlib4/pulls?q=is%3Apr+is%3Aclosed+label%3ALLM-generated
* Here's an attempt at a more subtle spectrum of labels: https://www.visidata.org/blog/2026/ai/#self-assessed-ai-level-for-contributions
* Lots of git commit messages ending in "Co-Authored-By: Claude ..." that's a pretty clear label and many coders now appear to be very happy to self-label with that.
* IMO the #podman AI policy is very sensible: https://github.com/containers/podman/blob/main/LLM_POLICY.md
The key terms (kind of labels) are not about whether an LLM was used but about readability, simplicity, conciseness, communication, understanding, and responsibility. -
@yoginho Perhaps not exactly the kind of "controlled labels" you are looking for, but here are some recent developments I've seen:
* the developer/maintainer of #syncthing is using the label "ai-slop" when rejecting certain PRs: https://github.com/syncthing/syncthing/pulls?q=is%3Apr+is%3Aclosed+label%3Aai-slop
* #mathlib uses the less emotionally charged label "LLM-generated": https://github.com/leanprover-community/mathlib4/pulls?q=is%3Apr+is%3Aclosed+label%3ALLM-generated
* Here's an attempt at a more subtle spectrum of labels: https://www.visidata.org/blog/2026/ai/#self-assessed-ai-level-for-contributions
* Lots of git commit messages ending in "Co-Authored-By: Claude ..." that's a pretty clear label and many coders now appear to be very happy to self-label with that.
* IMO the #podman AI policy is very sensible: https://github.com/containers/podman/blob/main/LLM_POLICY.md
The key terms (kind of labels) are not about whether an LLM was used but about readability, simplicity, conciseness, communication, understanding, and responsibility. -
So, just double-checking how #Lean4 and #Mathlib work:
* Lean takes 3GiB of RAM and a minute to open Mathlib
* Lean requires about 10min to build itself in CI, only verifying required theorems
* Verifying all of Mathlib is measured in hours
* Lean's kernel is untrustworthy due to junk theoremsAnd yet I'm a clown for using #Metamath? At some point we ought to reconsider the type-theory fetish.
-
The next bi-monthly #Mathlib community meeting is tomorrow Friday, 13th at 3pm UTC. Join to hear about ongoing #LeanLang formalization projects and connect with other contributors!
➡️ See all upcoming community events on our website: http://lean-lang.org/community/#events
-
The next bi-monthly #Mathlib community meeting is tomorrow Friday, 13th at 3pm UTC. Join to hear about ongoing #LeanLang formalization projects and connect with other contributors!
➡️ See all upcoming community events on our website: http://lean-lang.org/community/#events
-
"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
-
"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
-
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
-
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
-
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
-
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
-
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/ -
Domain specific (Documentation for Mathlib). ~ John Talbot, Richard M. Hill. https://www.renaissancephilanthropy.org/domain-specific-documentation-for-mathlib-1 #ITP #LeanProver #Mathlib
-
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 #автоматизация_доказательств #философия_математики
-
Growing Mathlib: maintenance of a large scale mathematical library. ~ Anne Baanen et als. https://arxiv.org/abs/2508.21593 #ITP #LeanProver #Mathlib
-
Growing Mathlib: maintenance of a large scale mathematical library. ~ Anne Baanen et als. https://arxiv.org/abs/2508.21593 #ITP #LeanProver #Mathlib
-
Lean Finder: Semantic search for Mathlib that understands user intents. ~ Jialin Lu et als. https://openreview.net/forum?id=5SF4fFRw7u #ITP #LeanProver #Mathlib
-
Lean Finder: Semantic search for Mathlib that understands user intents. ~ Jialin Lu et als. https://openreview.net/forum?id=5SF4fFRw7u #ITP #LeanProver #Mathlib
-
Readings shared May 10, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/10-readings_shared_05-10-25 #ITP #LeanProver #Math #Mathlib #Python
-
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
-
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
-
Basic probability in Mathlib. ~ Rémy Degenne. https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/ #ITP #LeanProver #Mathlib #Math
-
Basic probability in Mathlib. ~ Rémy Degenne. https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/ #ITP #LeanProver #Mathlib #Math
-
Readings shared February 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/05-readings_shared_02-05-25 #ITP #IsabelleHOL #LeanProver #Mathlib #LLMs #Math
-
Readings shared February 5, 2025. https://jaalonso.github.io/vestigium/posts/2025/02/05-readings_shared_02-05-25 #ITP #IsabelleHOL #LeanProver #Mathlib #LLMs #Math
-
A semantic search engine for Mathlib4. ~ Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, Bin Dong. https://arxiv.org/abs/2403.13310 #ITP #LeanProver #Mathlib
-
A semantic search engine for Mathlib4. ~ Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, Bin Dong. https://arxiv.org/abs/2403.13310 #ITP #LeanProver #Mathlib
-
As a step towards computer-formalizing the classification of low-dimensional Lie algebras, we finally formalized our first non-boring theorem in #Lean4 !
If L is a 3-dimensional Lie algebra (over any field) with a one-dimensional commutator subalgebra which is contained in the center of L, then L is isomorphic to the 3D Heisenberg algebra - that is, it has a basis (𝑒₀, 𝑒₁, 𝑒₂) such that the bracket is determined by
[𝑒₁,𝑒₂]=𝑒₀,
[𝑒₀,𝑒₁]=0,
[𝑒₀,𝑒₂]=0.Now we're working on the analogous results for higher dimensional commutator subalgebras. These are going to be harder because
a) there's no one-size-fits-all classification statement for arbitrary fields, and
b) they rely on certain normal forms of matrices which aren't yet implemented in #mathlib . -
The Matrix Cookbook, using Lean's mathlib. ~ Eric Wieser. https://github.com/eric-wieser/lean-matrix-cookbook #ITP #LeanProver #Lean4 #Mathlib #Math
-
The Matrix Cookbook, using Lean's mathlib. ~ Eric Wieser. https://github.com/eric-wieser/lean-matrix-cookbook #ITP #LeanProver #Lean4 #Mathlib #Math
-
Readings shared September 21, 2024. https://jaalonso.github.io/vestigium/posts/2024/09/21-readings_shared_09-21-24 #ITP #IsabelleHOL #LeanProver #Lean3 #Lean4 #Mathlib #Logic #Math #AI #LLMs #DeepLearning
-
Finding lemmas in Mathlib. ~ Damiano Testa. https://github.com/adomani/MA4N1_Theorem_proving_with_Lean/blob/master/MA4N1_2023/L17_navigating_Mathlib.lean #ITP #LeanProver #Mathlib
-
Lecturas compartidas el 1 de agosto de 2024. https://jaalonso.github.io/vestigium/posts/2024/08/02-lecturas_compartidas_el_01-ago-24 #ITP #Lean4 #Mathlib #Coq #Math #Haskell #FunctionalProgramming
-
Search Mathlib: A webpage that searches for Mathlib theorems. ~ Deming Xu. https://huggingface.co/spaces/dx2102/search-mathlib #ITP #Lean4 #Mathlib
-
LeanSearch: Find theorems in Mathlib4 using natural language query. https://leansearch.net #ITP #Lean4 #Mathlib
-
This month in Mathlib (May 2024). https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/ #ITP #Lean4 #Mathlib #Math
-
Lecturas compartidas el 14 de abril de 2024. https://jalonso.substack.com/lecturas-compartidas-el-14-de-abril #ITP #Lean4 #Mathlib
