The Best to Way to Learn Might Be Starting at the End: Writing a Proof in Lean (interjectedfuture.com)

A practitioner used an LLM to learn the Lean proof assistant by starting from a concrete goal: prove that Z-sets with pointwise (additive) merge form an abelian group. Practically, a Z-set is encoded as a function α → Int (a multiset/weight map that returns 0 for “not present”), and additive merge is defined pointwise: (zs1 + zs2)(x) = zs1 x + zs2 x. The learner asked the AI to generate a Lean tutorial that defines ZSet and ZSet.add, then to state an AbelianGroup typeclass (add, zero, neg plus add_zero, zero_add, add_inv, add_assoc, add_comm) and guide them to a working proof — finishing in a few hours with iterative, just-in-time explanations and translations (e.g., a Typescript “Rosetta stone”) to ground unfamiliar syntax. This workflow illustrates a shift in pedagogy: AI can collapse the “activation energy” of prerequisites so curiosity-led, end-goal-driven learning becomes feasible. For the AI/ML community this matters because it democratizes access to formal methods and niche tooling, enables bespoke tutorials and live translations between languages, and leverages proof assistants for verifiable answers. Caveats remain: success requires adjacent domain knowledge, skeptical questioning (LLM hallucinations), and domains with verifiable outcomes (math/proofs work especially well). The pattern — scope a concrete problem, have an LLM scaffold code and proofs, then iteratively ask for clarifications — shows a practical path for learning deep technical subjects end-first.