Re:An automatic theorem proving project
by deadbeef57 on Thursday April 28, 2022 @10:16AM
(#31192731)
Here's my guess.
Gowers wants to understand how the typical mathematician comes up with a proof. How is the proof found? Where do the ideas come from?
To some extent, this is orthogonal to whether or not you do maths constructively. But since 99.9% of mathematicians have never heard of constructive mathematics, and just use AoC or LEM all over the place, I am quite certain that Gowers is very much interested in how to find proofs in the "ordinary" sense: including the use of AoC and LEM.
Gowers wants to understand how the typical mathematician comes up with a proof. How is the proof found? Where do the ideas come from?
To some extent, this is orthogonal to whether or not you do maths constructively. But since 99.9% of mathematicians have never heard of constructive mathematics, and just use AoC or LEM all over the place, I am quite certain that Gowers is very much interested in how to find proofs in the "ordinary" sense: including the use of AoC and LEM.