solidSF Jesse · Lean output

What Jesse writes in Lean.

Statements the model emitted that compile on Lean 4.33 with no sorry, labelled by what they are. Compiling is the only claim made here.

Raw JSON Return to API

–

Compile · Lean 4.33, 0 sorry

–

Numeric identity

–

Ring identity

–

Propositional tautology

–

Inequality

–

Structural

–

Withdrawn · v1 BSD certificates

–

Contain sorry

–

With an axiom report

How to read this

Compiles

The kernel accepted it.

Lean 4.33 with Mathlib, no sorry. That is all the status says. Most entries are numeric or ring identities and propositional tautologies; the count by kind is above.

Topic

A label, not a result.

Topics name the area a statement was written for. A gauge-group dimension identity filed under Yang–Mills is still a dimension identity.

Withdrawn

The v1 BSD certificates.

Entries asserting #Sha = 1 from a numerical interval, with Lean files never compiled against Mathlib. Withdrawn 2026-09-22 and kept visible for the record.