Worked examples
The a + b = b + a example is on the home page →
Mathlib197: a new construction and three general lemmas
The matrix biproduct is rebuilt from identity-matrix entries, with no case splits or index transport.
Three general lemmas: ordered-partition sums for two and three, for the Faà di Bruno cases, and induction on the free
commutative ring, for Ring.DirectLimit.exists_of.
These changes in Lean, before and after
The run, and the declarations that changed most
Permanent: a new route from a longer search
A multi-step compression, for demonstration only, not ranked. Its new route: one parameter bound for all rational formulas (division by zero is zero) covers division-free ones too; derivations bound the dimension.
The route changes in Lean, before and after
Ramsey96: bounds re-derived from a sharper theorem
Its k log k bounds on the triangle Ramsey number follow in a few lines from a sharper theorem already in the file.
This change in Lean, before and after
The run, and the declarations that changed most
Compactness: small lemmas
Three brute-force case analyses became short arguments through small new lemmas,
cycle_map, kTemplateRelation_color_ne and retained_indicator_mul, measured
only together with other edits.
These changes in Lean, before and after
The run, and the declarations that changed most
All seven tasks at a glance
A range spans the two measured orders.
Toy targets one at a time or together
The fundamental theorem of arithmetic
A multi-step compression, for demonstration only, not ranked.
The agent's runs and checks
The agent's final: its terms and its Lean source
The natural original's largest auto-generated terms
The statements (the same in every version)
Every declaration: natural original and agent final
The hand compression: the version written long on purpose and its compressed form
It is long on purpose, with repeated re-derivations and automation instead of library lemmas.