1=0 Lean 4 Formalization of the Fundamental Arithmetic Contradiction
Abstract
We present a complete Lean 4 formalization demonstrating the collapse of the associative property in mixed number arithmetic. The expression 1(1/3)6 evaluates to 8 under left-association and 22/3 under right-association. Since associativity requires both values to be equal, we derive 8 = 22/3, leading to ⊥ (False) and consequently 1 = 0. All computational steps are verified by Lean 4's type checker.
Fields of Study & Subjects
Logic
programming
and type systems
History and Theory of Mathematics
Mathematics
Computing
and Information Processing
Publication details
- Journal / source
- Zenodo (CERN European Organization for Nuclear Research)
- Publication date
- 29 January 2026
- Language
- EN
- Document type
- Preprint