Search results

bound tactic does not work on level 1 of pset 3

Status: Open.

#120 In AlexKontorovich/RealAnalysisGame;

· dlebedinsky opened on Jun 17, 2026

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

Status: Open.

#118 In AlexKontorovich/RealAnalysisGame;

· Zeta-Wu opened on May 18, 2026

abs_Lipschitz breaks at about lecture 11

Status: Open.

#116 In AlexKontorovich/RealAnalysisGame;

· ketilwright opened on Apr 21, 2026

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

Status: Open.

#115 In AlexKontorovich/RealAnalysisGame;

· DERAlfons opened on Apr 16, 2026

Pset3 problem2 have incorrect setting

Status: Open.

#114 In AlexKontorovich/RealAnalysisGame;

· qlibp opened on Apr 13, 2026

Lecture 19 Level 2/4 Error in Description

Status: Open.

#112 In AlexKontorovich/RealAnalysisGame;

· KellyJDavis opened on Mar 10, 2026

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

Status: Open.

#109 In AlexKontorovich/RealAnalysisGame;

· daikonradish opened on Mar 4, 2026

Pset 24 Level 2 broken

Status: Open.

#102 In AlexKontorovich/RealAnalysisGame;

· AlexKontorovich opened on Jan 13, 2026

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

Status: Open.

#100 In AlexKontorovich/RealAnalysisGame;

· bluebear94 opened on Jan 4, 2026

Suggestion for L10PsetL10Pset3

Status: Open.

#99 In AlexKontorovich/RealAnalysisGame;

· sebroc opened on Jan 3, 2026

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

Status: Open.

#98 In AlexKontorovich/RealAnalysisGame;

· AlexKontorovich opened on Jan 2, 2026

Lecture 19 Level 2 needs mem_image and mem_range

Status: Open.

#97 In AlexKontorovich/RealAnalysisGame;

· AlexKontorovich opened on Jan 2, 2026