Re:AI solves IMO problems at silver medal level
by golol on Thursday July 25, 2024 @01:07PM
(#41070945)
Yea that's fair, but I don't think it will keep sucking forever as formalization is in principle just a translation process.
Re:AI solves IMO problems at silver medal level
by riku_iki on Thursday July 25, 2024 @03:04PM
(#41072195)
and we don't have 100% accuracy in translation in ambiguous texts, because system often need some domain knowledge, context etc. And math has 0% tolerance to mistakes.
I also expect that math formalized by machine will be readable by machine and hardly understandable by humans.
but this part currently sucks, because they didn't trust it and formalized problems manually.