Crossposted from X. source
I agree a lot with Martin Hairer. In competitive contest settings (like the IOI), the term “constructive” is used in a closely related but more informal sense. It refers to problems where the solver must design an explicit object, often a sequence, graph, or configuration, that satisfies specific constraints. Unlike theoretical deduction, these problems rely on creative observation. For example, a problem might ask one to reconstruct a sequence a with specific arithmetic properties from a permuted subsequence b. This requires the strategic selection of elements rather than the deduction of a single predetermined answer.
So constructive mathematics differs from classical mathematics by prioritizing explicit constructions and algorithmic proofs over abstract assertions of truth. It avoids “non-constructive” techniques, such as pure proof by contradiction or similar. In this setting, the phrase “there exists” essentially means “we can construct.” So a valid existence proof doesn’t assert that an object is logically necessary but it provides a method or procedure for finding it.
today’s RL paradigm models do not truly “understand” the proofs they generate. The more “mechanical” a problem is, the more amenable it is to incremental verification. GDMs iterations of alphaproof are fundamentally pretty similar just with a more efficient search and a lot more compute. I’m sure we will find proofs to a lot of unsolved problems and this in a way for sure will speed up some mathematicians research progress (i talked a lot about which math subjects are more prone to this), but a lot of the work a mathematician does is to clarify which questions to ask in the first place, what is interesting to actually work on. Without a fundamental change this approach will not generate any deep fundamental novel insights and ideas. To be clear I’m not saying that there isn’t any progress and this is completely worthless. I think just a lot of ppl get the implications wrong.
You must understand that Putnam and the IMO require very different skillsets and training than mathematical research. You can get gold at the IMO but be a bad mathematician and vice versa. Actually from experience, the IMO maps a lot ways of thinking that can be compared with competitive programming. I got grandmaster in under a year on Codeforces because I had years of mathematical olympiad training before, which unknowingly trained me to learn these types of competition problems faster and gave me a huge advantage in a bet I had with a friend who could reach grandmaster first.