"The truly correct proof is one that strikes a harmonious balance between strength and flexibility. There are plenty of proofs that are technically correct but are messy and inelegant or counterintuitive. But it's not something you can put into words—explaining why a formula is beautiful is like trying to explain why the stars are beautiful."
Yōko Ogawa: The housekeeper and the professor
Any artificially generated mathematical text will not be considered as a proof unless:
- It has been communicated in both a natural language text paired with a computer formalization of all definitions, theorems, and proofs.
- The formalization has been accepted by the proof assistant and human expert referees have vetted both the formalization and the paired text.
Unlike Gentzen, we can make use of css and javascript
Paperproof README
Is it still a proof if it takes 4 minutes on a 4 GHz 12-core CPU?
Beware of bugs in the above code;
I have only proved it correct, not tried it.
