Thread

1. fspeech · 1789802226 · focus · HN ↗

   I enjoy learning math from LLM proofs with the help of LLMs <a href="https:&#x2F;&#x2F;github.com&#x2F;htzh&#x2F;flt_for_human" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;htzh&#x2F;flt_for_human . It is amazing how well models do when they are well grounded by formalized proof traces (even if created by other models).

   1. Smaug123 · 1789804039 · focus · HN ↗

      I&#x27;d be interested in hearing a field report on this! For example, I can easily imagine that they&#x27;re great at walking through the proof step by step, explaining background as necessary; but as TFA notes, one of the most important questions is &quot;why is this definition the way it is?&quot;, and my bet would be that the Lean is not enough to help the LLMs meaningfully in answering that.

      1. someguynamedq · 1789811281 · focus · HN ↗

         Fortunately LLMs are smart enough to handle that already.

Unofficial Hacker News client; not affiliated with Y Combinator.