Slacker News Slacker News logo featuring a lazy sloth with a folded newspaper hat
  • top
  • new
  • show
  • ask
  • jobs
Library
← Back to context

Comment by david-gpu

5 days ago

Proof assistants like Lean are there to catch any errors. Now, can you just feed the error logs back to the AI and let it iteratively fix any mistakes? I don't know, I haven't used those things in two decades.

1 comment

david-gpu

Reply

Jaxan  5 days ago

You still need a mathematician to check the statement of the theorem.

Slacker News

Product

  • API Reference
  • Hacker News RSS
  • Source on GitHub

Community

  • Support Ukraine
  • Equal Justice Initiative
  • GiveWell Charities