Issues

• Lecture 19 Level 4: Cannot pass the level by typing "sorry"

  AlexKontorovich/RealAnalysisGame#128 · Filter by author xnuk opened on Oct 2, 2026

• Failure in lecture3/1 "The Archimedean Property"

  AlexKontorovich/RealAnalysisGame#127 · Filter by author yihuang opened on Sep 26, 2026

• Lecture 19: Should introduce how to use Nonempty

  AlexKontorovich/RealAnalysisGame#126 · Filter by author xnuk opened on Sep 23, 2026
  1

• Downloaded save file contains nothing

  AlexKontorovich/RealAnalysisGame#124 · Filter by author nsw50 opened on Aug 3, 2026
  1

• When applying the tactic from the sidebar, clicking "rewrite" enters "rw" in the command line.

  AlexKontorovich/RealAnalysisGame#123 · Filter by author abhavsar232 opened on Jul 28, 2026

• Lecture 12 Notes

  AlexKontorovich/RealAnalysisGame#122 · Filter by author Babagilo opened on Jul 22, 2026

• Can't get past Lecture 19 Level 4 under Regular rules

  AlexKontorovich/RealAnalysisGame#121 · Filter by author lilyball opened on Jul 18, 2026
  1

• bound tactic does not work on level 1 of pset 3

  AlexKontorovich/RealAnalysisGame#120 · Filter by author dlebedinsky opened on Jun 17, 2026

• Level 1 in Lecture 23 needs more Theorems to solve; otherwise the codes get too chunky

  AlexKontorovich/RealAnalysisGame#118 · Filter by author Zeta-Wu opened on May 18, 2026

• abs_Lipschitz breaks at about lecture 11

  AlexKontorovich/RealAnalysisGame#116 · Filter by author ketilwright opened on Apr 21, 2026

• Missing tag / branch for toolchain v4.26.0 in lean4game repository

  AlexKontorovich/RealAnalysisGame#115 · Filter by author DERAlfons opened on Apr 16, 2026

• Pset3 problem2 have incorrect setting

  AlexKontorovich/RealAnalysisGame#114 · Filter by author qlibp opened on Apr 13, 2026

• Lecture 19 Level 2/4 Error in Description

  AlexKontorovich/RealAnalysisGame#112 · Filter by author KellyJDavis opened on Mar 10, 2026

• ring_nf interacts confusingly with the UI when provided with a typo.

  AlexKontorovich/RealAnalysisGame#109 · Filter by author daikonradish opened on Mar 4, 2026

• Pset 24 Level 2 broken

  AlexKontorovich/RealAnalysisGame#102 · Filter by author AlexKontorovich opened on Jan 13, 2026

• Lecture 8 Level 1 doesn’t actually need by_cases hk0 : k = 0

  AlexKontorovich/RealAnalysisGame#100 · Filter by author bluebear94 opened on Jan 4, 2026

• Suggestion for L10PsetL10Pset3

  AlexKontorovich/RealAnalysisGame#99 · Filter by author sebroc opened on Jan 3, 2026

• Lecture 7 Level 3: explain that ||a n| - |L|| will fail without parentheses

  AlexKontorovich/RealAnalysisGame#98 · Filter by author AlexKontorovich opened on Jan 2, 2026

• Lecture 19 Level 2 needs mem_image and mem_range

  AlexKontorovich/RealAnalysisGame#97 · Filter by author AlexKontorovich opened on Jan 2, 2026
  1

• Pset 1 Level 5 (and Level 1) is trivially solvable

  AlexKontorovich/RealAnalysisGame#96 · Filter by author AlexKontorovich opened on Jan 2, 2026

• Suggestion for L10LevelsL09_Subseq

  AlexKontorovich/RealAnalysisGame#95 · Filter by author sebroc opened on Jan 2, 2026

• Typos in L9LevelsL05_BddOfConv

  AlexKontorovich/RealAnalysisGame#92 · Filter by author sebroc opened on Dec 30, 2025

• Rendering issue in L9LevelsL05_BddOfConv

  AlexKontorovich/RealAnalysisGame#91 · Filter by author sebroc opened on Dec 30, 2025

• RorQ class in the Cauchy sequences / Bolzano-Weierstrass levels

  AlexKontorovich/RealAnalysisGame#90 · Filter by author AlexKontorovich opened on Dec 29, 2025

• Consider allowing abs_sub

  AlexKontorovich/RealAnalysisGame#89 · Filter by author ada4a opened on Dec 28, 2025