• by meltyness on 5/13/2025, 10:59:49 AM

    Lean is a lovely language ecosystem, as Tao clearly demonstrates though, LLMs can struggle with it. The language and the tooling is designed heavily around not merely text code, but continuous feedback from a specialized shell, though Tao attributes the issue to another condition, that there are two acutely similar versions of the language.

  • by AntoniusBlock on 5/14/2025, 10:41:05 AM

    Slightly offtopic, but there are other Fields Medalists on youtube too, such as Richard E Borcherds. He has some very nice videos on number theory and abstract algebra.

    https://www.youtube.com/@richarde.borcherds7998

  • by KiranRao0 on 5/13/2025, 8:23:17 AM

    Can someone provide a tl;dr on him/why he’s important?