https://news.ycombinator.com/user?id=kameamaHacker News RSShttps://hnrss.org/hnrss v2.1.1Fri, 17 Apr 2026 13:04:45 +0000I'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.

]]>Tue, 10 Mar 2026 15:26:46 +0000https://news.ycombinator.com/item?id=47324575kameamahttps://news.ycombinator.com/item?id=47324575https://news.ycombinator.com/item?id=47324575A 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

]]>Mon, 09 Mar 2026 04:43:00 +0000https://news.ycombinator.com/item?id=47304953kameamahttps://news.ycombinator.com/item?id=47304953https://news.ycombinator.com/item?id=47304953