News for hackers. Stuff that matters.
Re:AI solves IMO problems at silver medal level by riku_iki on Thursday July 25, 2024 @01:04PM (#41070917)
> They are building a general pipeline which turns informal natural lamguage mathematics

but this part currently sucks, because they didn't trust it and formalized problems manually.

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.