Comment by 2snakes
1 day ago
Said like a true formalist. Mathematical insight is a pretty creative act of consciousness. The formalization of it tends to come after.
1 day ago
Said like a true formalist. Mathematical insight is a pretty creative act of consciousness. The formalization of it tends to come after.
You have a point about insight and creativity but I feel you are discounting the value of formal proofs too much. Modern math has a kind of reproducibility crisis in that the number of people who can actually verify recent proofs is often less than 10. There are thousands of proofs that were verified by a few people who are now dead. Should we consider them to still be proven?
Most recent proofs are just as much of a black box to nearly all mathematicians as a 200,000 line Lean proof is.