Here’s an example of what I think you mean by “proofs and conclusions constructed in very abstracted, and not experimentally or formally verified math”:
Given two intersecting lines AB and CD intersecting at point P, the angle measure of two opposite angles APC and BPD are equal. The proof? Both sides are symmetrical so it makes sense for them to be equal.
On the other hand, Lean-style proofs (which I understand you to claim to be better) involve multiple steps, each of which is backed by a reasoning step, until one shows that LHS equals RHS, which here would involve showing that angle APC = BPD:
angle APC + angle CPB = 180 * (because of some theorem)
angle CPB + angle BPD = 180 * (same)
[...]
angle APC = angle BPD (substitution?)
There’s a sense in which I feel like this is a lot more complicated a topic than what you claim here. Sure, it seems like going Lean (which also means actually using Lean4 and not just doing things on paper) would lead to lot more reliable proof results, but I feel like the genesis of a proof may be highly creative, and this is likely to involve the first approach to figuring out a proof. And once one has a grasp of the rough direction with which they want to prove some conjecture, then they might decide to use intense rigor.
To me this seems to be intensely related to intelligence (as in, the AI alignment meaning-cluster of that word). Trying to force yourself to do things Lean4 style when you can use higher level abstractions and capabilities, feels to me like writing programs in assembly when you can write them in C instead.
On the other hand, it is the case that I would trust Lean4 style proofs more than humanly written elegance-backed proofs. Which is why my compromise here is that perhaps both have their utility.
They definitely both have their validity. They probably each also make some results more salient than other results. I’d guess in the future there’ll be easier Lean tools than we currently have, which make the practice feel less like writing in Assembly. Either because of clever theorem construction, or outside tools like LLMs (if they don’t become generally intelligent, they should be able to fill in the stupid stuff pretty competently).
Here’s an example of what I think you mean by “proofs and conclusions constructed in very abstracted, and not experimentally or formally verified math”:
Given two intersecting lines AB and CD intersecting at point P, the angle measure of two opposite angles APC and BPD are equal. The proof? Both sides are symmetrical so it makes sense for them to be equal.
On the other hand, Lean-style proofs (which I understand you to claim to be better) involve multiple steps, each of which is backed by a reasoning step, until one shows that LHS equals RHS, which here would involve showing that angle APC = BPD:
angle APC + angle CPB = 180 * (because of some theorem)
angle CPB + angle BPD = 180 * (same)
[...]
angle APC = angle BPD (substitution?)
There’s a sense in which I feel like this is a lot more complicated a topic than what you claim here. Sure, it seems like going Lean (which also means actually using Lean4 and not just doing things on paper) would lead to lot more reliable proof results, but I feel like the genesis of a proof may be highly creative, and this is likely to involve the first approach to figuring out a proof. And once one has a grasp of the rough direction with which they want to prove some conjecture, then they might decide to use intense rigor.
To me this seems to be intensely related to intelligence (as in, the AI alignment meaning-cluster of that word). Trying to force yourself to do things Lean4 style when you can use higher level abstractions and capabilities, feels to me like writing programs in assembly when you can write them in C instead.
On the other hand, it is the case that I would trust Lean4 style proofs more than humanly written elegance-backed proofs. Which is why my compromise here is that perhaps both have their utility.
They definitely both have their validity. They probably each also make some results more salient than other results. I’d guess in the future there’ll be easier Lean tools than we currently have, which make the practice feel less like writing in Assembly. Either because of clever theorem construction, or outside tools like LLMs (if they don’t become generally intelligent, they should be able to fill in the stupid stuff pretty competently).