Learning games for the proof assistant Lean | Dark Hacker News