alt Hacker NewsI am a math undergrad and I tried lean. It probably is because of habit and familiarity but I still find lean proofs harder to read than NL proofs. I wonder what if the math education switch entirely to a formal language (not necessarily Lean) will be?
Replies
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/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
"Mathematics is commonly explained and recorded in symbolic and concrete forms that are easy to communicate, rather than in conceptual forms that are easy to understand once communicated. Translation in the direction conceptual -> concrete and symbolic is much easier than translation in the reverse direction, and symbolic forms often replaces the conceptual forms of understanding."
https://mathoverflow.net/questions/43690/whats-a-mathematici...
i feel like this would be the equivalent of having all CS undergrads program with assembly and assembly only.
it might(?) work? but abstractions exist for a reason (mostly...)
Ask a model (dsv4.1 flash works great on this) to explain the proof to you so you can get an idea of the overall concept and structure first. Formalized math tends to encode math a certain way to make it easier for Lean, which doesn't have a visual cortex, but harder for people.