HARD PROBLEMS · AUGUST–SEPTEMBER 2026 · STOPPED AFTER PRIOR-WORK CHECK
The formal package passed its machine checks and remains available under a public DOI. I later confirmed that the same conclusion and a Lean formalization predated my work, and I ended the publication path.
In August 2026 I constructed an explicit infinite countermodel showing that Ulrich’s u4 is not a single axiom for positive implicational logic. I froze the package after a Lean kernel build, a separate symbolic check, an axiom audit, and source scans.
What the package established
The recorded Lean 4.30.0 build exited successfully. The decisive file contained no sorry, admit, user-defined axiom, or opaque workaround, and the independent checker passed. The package received a public archival record on August 21.
What the first search missed
My initial public search did not find an equivalent proof. Follow-up with relevant researchers established that the same result, including a Lean verification, had appeared several months earlier. The journal record closed on September 2 for overlap with prior work. I do not reproduce the private correspondence or decision text.
A proof assistant can check whether an object satisfies its formal obligations. It cannot tell me whether the result is new. The formalization remains reusable, but it is not a first proof, a new theorem, or a peer-reviewed publication.
Project record
Period: August 21–September 2, 2026
Activity: construction of an infinite countermodel, Lean formalization, independent checks, and public archiving
Internal evidence: formal source, verification logs, a symbolic checker, hashes, and scope documents
External validation: a public Zenodo DOI and CI record; researcher confirmation and a closed journal record
Final outcome: machine verification completed, novelty absent, no peer-reviewed publication
Withheld: researcher and editor names, private messages and decision text, and submission identifiers