Zulip Chat Archive

Stream: general

Topic: LeanGameServer x Undergrad Math ?

TongKe Xue (Dec 07 2025 at 00:26):

I'm a big fan of (LeanGameServer) https://adam.math.hhu.de/

Is there something like LeanGameServer x Undergrad Math, where you can work through the entire curriculum interactively, and have Lean provide "instant feedback" (at the cost of 5x-10x longer proofs) ?

Patrick Massot (Dec 07 2025 at 09:37):

No there isn’t.

TongKe Xue (Dec 07 2025 at 10:58):

Off topic, but your work on "verbose lean" looks really cool. Almost reads like a formal human proof, rather than humans trying to write formal lean4 proofs.

TongKe Xue (Dec 08 2025 at 00:00):

Are the closest resources to this

  1. https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html
  2. collection of courses taught in Lean
    ?

[I have in mind something 'gamified' like Khan Academy math courses, but done in Lean4, with the "fun" of the LeanGameServer, and covering most of the undergrad curriculum. ]

Last updated: Dec 20 2025 at 21:32 UTC