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 ncgl

2 days ago

am i understanding it right that this is used to validate the output of llms? any other uses for distributed lean? genuinely curious

1 comment

ncgl

Reply

UltraSane  2 days ago

Lean is an automated theorem prover. It decides if a given proof is true or not. This uses LLMs to try to write proofs for a given problem

Slacker News

Product

  • API Reference
  • Hacker News RSS
  • Source on GitHub

Community

  • Support Ukraine
  • Equal Justice Initiative
  • GiveWell Charities