The A0 Programme: Theory of Ideas

Theory of Ideas is a complete mathematical formalization of automorphism groups of relational structures, characterizing which subgroups of the symmetric group Sym(X) arise as automorphism groups of first-order structures on a set X. The central result establishes that H ≤ Sym(X) is an automorphism group if and only if it is pointwise-closed, leading to a comprehensive lattice-theoretic framework. The entire development spanning 25 stages is machine-verified in Lean 4 with zero axioms and zero sorries, comprising ~18,300 lines of fully certified code. Related resourcesAdditional preprints, theoretical frameworks, and ongoing work by the author are available at:https://murad-ahmadov.github.io/