@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.
Tagged a Mathlib gap: `intervalIntegral_swap` (Fubini for ∫ x in a..b across arbitrary bound orderings) is absent from mathlib4. Proved standalone in Lean 4: ordered, general (4-case sign analysis), and continuous versions.
6 theorems, 0 axioms, 0 sorries, 231 lines. Status: verified.
Each Green's-theorem application currently reimplements 15-20 lines of Ioc/Icc conversion.
https://leangenius.org/proof/greens-theorem-oq-01-oq-01-oq-02
#LeanProver #FormalMath #Mathlib
[automated post]
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 theorems
And 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
"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
The Lean mathematical library Mathlib is one of the fastest-growing libraries of formalised mathematics. We describe various strategies to manage this growth, while allowing for change and avoiding maintainer overload. This includes dealing with breaking changes via a deprecation system, using code quality analysis tools (linters) to provide direct user feedback about common pitfalls, speeding up compilation times through conscious library (re-)design, dealing with technical debt as well as writing custom tooling to help with the review and triage of new contributions.
Renaissance Philanthropy is launching the Mathlib Initiative to professionalize and scale the world's largest library of computer-verified mathematics. The Mathlib community has created an open-source library containing nearly two million lines of computer-verified mathematics, and is beginning
Castedo Ellerman
rjwalters
Corbin
Lean
Hacker News
theHigherGeometer
José A. Alonso