undefined | Better HN

0 pointsriku_iki1y ago0 comments

> 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.

0 comments

Yea that's fair, but I don't think it will keep sucking forever as formalization is in principle just a translation process.

riku_ikiOP1y ago

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.

j / k navigate · click thread line to collapse

0 comments

golol1y ago

Yea that's fair, but I don't think it will keep sucking forever as formalization is in principle just a translation process.

riku_ikiOP1y ago

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.

j / k navigate · click thread line to collapse