Re:An automatic theorem proving project
by adamnemecek on Thursday April 28, 2022 @10:07AM
(#31192623)
I wonder if this will be constructivist.
[ Parent
| on HN ]
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.
Re:An automatic theorem proving project
by auggierose on Thursday April 28, 2022 @10:59AM
(#31193272)
No, it won't be.