4 ms·
> They are building a general pipeline which turns informal natural lamguage mathematics but this part currently sucks, because they didn't trust it and formal
by riku_iki 2y ago
> 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.
- golol 2y agoYea that's fair, but I don't think it will keep sucking forever as formalization is in principle just a translation process.
- riku_iki 2y agoand 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.