alt Hacker NewsAs 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/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
Replies
xiaoyu2006 • yesterday at 6:40 PM
[dead]
Putting aside the Claudisms.
You only compare to tactic heavy languages, which is what you don't like about them. Try looking at Agda, Idris, Mikan,... They work with pattern matching not just for definitions but for proofs as well, so the derivation is laid bear.
Not saying your niche doesn't have value, but you can get interesting ideas from there.