Issues

• 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

• Retry button works in unexpected way

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

• 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
  1

• Add a way to reveal missed hints

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

• 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

• (Number Theory Game) dvd_antisymm not available

  leanprover-community/NNG4#175 · Filter by author cbuccheri opened on Sep 29, 2026
  1

• 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

• I run the game in local, after I complete Tutorial world(finish the first boss), I still can't continue to the next World

  leanprover-community/NNG4#153 · Filter by author zzz6519003 opened on Jun 3, 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
  2

• 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

• Victory condition achieved when writing non sensical tactics

  buglean4game
  leanprover-community/NNG4#103 · Filter by author astrale-sharp opened on Jun 26, 2025
  6