Skip to content
Better HN
Top
Best
Ask
Show
New
Jobs
Search
⌘K
0 points
jeremyjh
1y ago
0 comments
Save
Share
Yes and it is difficult for me to believe that there is not useful human analysis and understanding involved in this translation that the AI is helpless without. But that I suppose is a problem that could be tackled with a different model...
0 comments
2 comments · 2 top-level
top
newest
oldest
adrianN
1y ago
Even so, having a human formalize the problems and an AI to find machine checkable proofs could be very useful for mathematicians.
sebzim4500
1y ago
It is vastly easier to do the formalization than to actually solve the problem. Any undergraduate with some lean familiarity could do it in minutes.
1 more reply
j
/
k
navigate · click thread line to collapse