Issues

• natural number game: "can't access property Symbol.iterator of undefined"

  leanprover-community/NNG4#194 · Filter by author dandrake opened on Nov 12, 2026

• Typewriter mode: lines after a failed rw are silently ignored (Tutorial level 8)

  leanprover-community/NNG4#191 · Filter by author jesusholoo opened on Nov 9, 2026
  1

• Slightly awkward wording in level 3 of the first world

  leanprover-community/NNG4#189 · Filter by author Iurig opened on Oct 25, 2026

• Crash frequency increasing in the Natural Number Game

  leanprover-community/NNG4#188 · Filter by author espressonator opened on Oct 23, 2026
  2

• In Multipl

  leanprover-community/NNG4#184 · Filter by author espressonator opened on Oct 2, 2026
  1

• Pasting works unintuitively in Babylon Level 7 / 9

  leanprover-community/NNG4#183 · Filter by author ByteEater-pl opened on Oct 2, 2026
  1

• Retry button potentially loses much work

  leanprover-community/NNG4#182 · Filter by author ByteEater-pl opened on Oct 2, 2026
  1

• Retry button works in unexpected way

  leanprover-community/NNG4#181 · Filter by author ByteEater-pl opened on Oct 2, 2026
  1

• Persistent error state in which it only seems possible to continue a proof

  leanprover-community/NNG4#180 · Filter by author ByteEater-pl opened on Oct 1, 2026
  2

• Suboptimal hint in Level 9 / 10 : mul_left_cancel

  leanprover-community/NNG4#178 · Filter by author ByteEater-pl opened on Sep 30, 2026

• Cannot rewrite LHS of inequality

  leanprover-community/NNG4#177 · Filter by author ByteEater-pl opened on Sep 30, 2026

• Unable to use add_left_comm in Level 7 / 9 : mul_add

  leanprover-community/NNG4#176 · Filter by author ByteEater-pl opened on Sep 30, 2026

• Unable to download the progress file

  leanprover-community/NNG4#173 · Filter by author jmgimeno opened on Sep 26, 2026

• Update Game.pot & translation files

  leanprover-community/NNG4#171 · Filter by author TentativeConvert opened on Sep 10, 2026
  2

• minor feature request: a way to turn Fermat's Last Bubble green

  leanprover-community/NNG4#167 · Filter by author TentativeConvert opened on Aug 26, 2026
  2

• Natural Number World: Level 7 - rw [one_eq_succ_zero] doesn't expand 1

  leanprover-community/NNG4#155 · Filter by author jochasinga opened on Jun 21, 2026

• le_antisymm hints

  leanprover-community/NNG4#148 · Filter by author comods opened on May 15, 2026

• Better ≤ World 5th Level hints

  leanprover-community/NNG4#146 · Filter by author comods opened on May 15, 2026

• succ_mul level has a bad hint

  leanprover-community/NNG4#141 · Filter by author comods opened on May 9, 2026

• No Goals and Level is not Completed

  leanprover-community/NNG4#140 · Filter by author comods opened on May 8, 2026
  3

• Escape sequences are missing from inventory right side panel

  leanprover-community/NNG4#139 · Filter by author comods opened on May 6, 2026
  1

• Power World level 5 doesn't allow rewrites

  leanprover-community/NNG4#138 · Filter by author aadi07 opened on Apr 29, 2026
  1

• Explanation for rfl

  buglean4game
  leanprover-community/NNG4#131 · Filter by author yerke opened on Mar 5, 2026
  1

• Unclear description of Algorithm World 7

  documentation
  leanprover-community/NNG4#111 · Filter by author joneugster opened on Aug 8, 2025
  1

• A new out-of-the-box docker image

  enhancement
  leanprover-community/NNG4#110 · Filter by author ovo-Tim opened on Jul 31, 2025
  3