A 16×16 multiplication table that encodes quoting, evaluation, branching, recursion, an 8-state counter, and IO — all as lookups in the same table. 83 Lean theorems, zero sorry.
The project asks: can a finite algebra with a single binary operation be forced by axioms to contain its own representation layer? The answer is yes. Axiom-driven SAT search finds the constraints, Lean verifies the witness.
I should be upfront: Claude wrote most of the Lean proofs and Z3 search scripts. My role was the ontological framework, the axiom design, and deciding what to search for and why. The AI-human split was roughly: I provided the "what should exist and why," Claude provided the "here's the code that proves/finds it." Every Lean theorem compiles independently regardless of who typed it.
Universal results (hold for all satisfying algebras, not just this table): every model is rigid, judgment and synthesis provably cannot commute, and the tester's acceptance partition carries irreducible information that structure alone can't determine.
The specific table fits in 256 bytes and can be recovered from a shuffled black-box oracle in 62 probes.
https://github.com/stefanopalmieri/Kamea
I'm working on a paper but it will take some number of years. But it will take some time. The github repo has some documentation but admittedly does need work.
You could publish preliminary versions of your paper on Zenodo. This way you get a DOI and can claim authorship, and work on it until it is ready to be submitted somewhere. It seems to me you could already write something interesting now. The github repo docs are quite cryptic, and I have no clue what they are trying to tell me :-)
