Standalone mathematical publications
Papers, manuscripts, and notes
Read mathematical papers, manuscripts, working notes, expositions, and research roadmaps. These publication pages are distinct from the active research workspaces for open conjectures. Each page keeps its formalization status explicit: publication or editorial review is not a substitute for a Lean-checked proof.
A Formalized Proof of Bondy's Minimum-Degree Longest-Cycle Conjecture
Lech Mazur's August 16 paper presents a candidate proof of Bondy's minimum-degree longest-cycle conjecture. Paper-to-formal-statement alignment is under review. Lean checks only the exact displayed endpoint Bondy.bondy_longest_cycle at audited source commit 9e13b044…. The retained release audit covers its 204-module dependency cone, reports no project mathematical axioms or sorry, and records only standard classical foundations; independent acceptance and specialist review remain open.
Fully formalizedResearch paperAn Exact Counterexample to Berlekamp's Temperature-2 Conjecture for Domineering
Lech Mazur's manuscript gives a rectangle-reachable 28-cell Domineering position with exact game {17/8 | -2+*} and temperature 33/16 > 2. The attached Lean development kernel-checks the board–target equality, explicit target thermograph, 30-move replay, and resulting existential statement through its narrow HasValueTemperature interface; unrelated external replication and specialist review remain open.
Partially formalizedResearch paperA Computer-Assisted Proof Candidate for Sendov's Conjecture
Lech Mazur's public Revision 16 presents a self-contained computer-assisted proof candidate for Sendov's conjecture, with exact rational terminal certificates, deterministic regeneration, mutation tests, and an explicit boundary between machine-checked computation and the written analytic reduction.
Latest listed version · Formalization plannedResearch paperA Simplified Proof Candidate for Sendov's Conjecture with Exact Rational Certificates
Lech Mazur's public Revision 14 presents an all-degree computer-assisted proof candidate for Sendov's conjecture, supported by exact rational terminal certificates and accompanied by an explicit boundary between checked computation and written analysis.
Earlier listed version · Formalization planned