12 / Research methods Research method
Small proofs. Made to travel.
From a computational need to a lemma someone else can use.
The lemma atelier starts with a calculation that needs a general statement. A candidate moves through attempts to falsify it, a proof, independent review, and an explicit boundary of applicability.
The six recorded lemma dossiers cover disjoint blockers; first-moment blindness to invariant features; symmetry restrictions for no-four-coplanar sets; expected collinear triples; a line model for direction spectra; and the HJSW-window theorem.
Formalisation is tracked separately: parts of the first and third dossiers have Lean developments. This is not a claim that every lemma, hypothesis or concrete model has been fully formalised.
Where the claim stops.
The dossiers distinguish proofs, finite checks, partial formalisation and known results reused as corollaries.
Source: lemma-atelier / README.md. Summary prepared from the local research record, 11 September 2026.
Research led by Aleksei Kudriashov (Alex Komang). Mathematical paper and witness text/data: CC BY 4.0 where stated in the source repository.