alt Hacker NewsThat makes some sense. Given that the vast majority of math in its training data is going to be in NL/latex, I just assumed that the core reasoning happens in NL with occasional LEAN checks to ensure validity.
That makes some sense. Given that the vast majority of math in its training data is going to be in NL/latex, I just assumed that the core reasoning happens in NL with occasional LEAN checks to ensure validity.