News for hackers. Stuff that matters.
Re:AlphaProof's Greatest Hits: the coolest bits from the IMO... by andrepd on Sunday November 17, 2024 @05:58PM (#42168126)
More or less. Modern theorem provers, even fully automatic ones, can prove incredibly difficult problems if given enough time. With 3 days and terabytes of memory, perhaps they could? Would be interesting to compare Alphaproof with a standard theorem prover that is given similarly astronomical computing resources.
Re:AlphaProof's Greatest Hits: the coolest bits from the IMO... by auggierose on Sunday November 17, 2024 @06:18PM (#42168238)
That is an interesting thought. But I doubt that standard automated theorem proving techniques would have solved this in a 100 years, even with immense resources, as all they do is (basically) brute force search, and it remains an exponential search space. Therefore 3 days does not really matter, indeed, 3 months would still be a result that 10 years ago I would have thought impossible.