Thread

If math is more than proof, we need to better celebrate the rest of it

433 points · 285 comments · num42

bobajeff · 1789827473 · focus · HN ↗
Let's see how long (if it ever happens) it takes for models to generate motivated explanations (possibly done via the Manim library or something like it) along with their Lean proofs. Grant Sanderson is right that this is kind of subjective but so is Art and I'm very enthusiastic about AI generated Art.
1. zozbot234 · 1789830961 · focus · HN ↗
  > possibly done via the Manim library or something like it
  It can be done already: the point is that the motivation and explanation parts are terrible, especially for novel topics where the AI can't just rip off existing content. A Lean proof is at least a verifiable task; you end up with an actual proof that you can work through. A Manim slop video doesn't have that.

Unofficial Hacker News client; not affiliated with Y Combinator.