Naoki Takata
January 10, 2026
We investigate the problem of determining all positive integers n for which there exists a triangle that can be dissected into n congruent triangles. We prove that such a dissection is possible if and only if n ≠ 5. This result combines elementary constructions for small cases with the deep impossibility result for n = 5 due to Tutte (1965). We provide a complete characterization and discuss the key ideas behind the proof.
As a proof of existence for this paper, the Keccak-256 hash of the PDF has been recorded on the Ethereum blockchain.
Timestamp: January 10, 2026 (date recorded on the blockchain)
All theorems are formalized in Lean 4 (Mathlib commit f897ebcf72cd16f89ab4577d0c826cd14afaafc7). The verification used Aristotle, an automated theorem proving system for Lean 4.
Naoki Takata
X: @naokitakata
Email: [ntakata [at] proton.me]
This is a preprint. Comments are welcome!