Carlo Perassi

A second Sep 8 session on the Diaz tree closed the free half: no admissible matrix exists there, and that is now proved, after which norm_free closes onto the published statement (S) and the frontier stands at four leaves. The log also publishes an SFE route the session’s other model proved and withheld, records the lesson that the relation you are using is the one that breaks your argument, and scopes the next target with a brief for the four-exponentials theorem at transcendence degree one.

carlok/prove2me-logs is the working log of my Prove2Me formalization activity — per-mission entries with theorem uuids, Lean environments, and what remains open — public since Sep 7 as a record of the work rather than an archive of the proofs. The first entries record dead ends beside progress: the free-ring no-go formalized with its prose proof intact, a six-exponentials no-go note with a Waldschmidt erratum, and a Diaz bridge node that turned out to attach to nothing. Day two records the Diaz tree and writes up the decompose–link–iterate rule behind it: by the fourth generation the main theorem’s difficulty sits in a single named leaf — pi transcendence — with both leaves of the second branch named.

carlok/unused-assumptions is a new public repository (visible since Sep 4; v1.0–v1.2 tagged Sep 6, archived at doi:10.5281/zenodo.22549525): theorems in Mathlib whose stated algebraic setting is stronger than their own proof requires. The method is one sentence — take a theorem, replace one binder with a weaker class, keep the proof byte for byte, compile it alone — and every row of data/survivors.jsonl carries what is needed to put the claim back in front of the compiler. A verifier rechecks each row at the Mathlib revision the manifest names, refuses to run against a different one, and requires #print axioms to rest on nothing beyond propext, Classical.choice and Quot.sound. Re-verifying the 36 candidate patches against a later Mathlib kept the 33 that still hold, and the README now answers the prior-art question explicitly rather than leaving it to the reader.