Comment Comment by dnautics As a former math major (and developer) it bugged me that lean is optimized for WRITING proofs and not for READING proofs. I'm noodling around with a language that is optimized for reading proofs:https://github.com/ityonemo/2b4mThe tradeoff is that it's more verbose, but you don't have to even know the language to properly decode a proof.as an exercise for the language, I'm playing around with having Claude formalize an online algebra text:https://github.com/ityonemo/2b4m/tree/main/aataLMK what you think parent dnautics 15 days ago
https://github.com/ityonemo/2b4m
The tradeoff is that it's more verbose, but you don't have to even know the language to properly decode a proof.
as an exercise for the language, I'm playing around with having Claude formalize an online algebra text:
https://github.com/ityonemo/2b4m/tree/main/aata
LMK what you think