Issues

• Hardcoded identifier in hint in Epo Level 4 / 7

  hhu-adam/Robo#194 · Filter by author ByteEater-pl opened on Oct 6, 2026

• Hint too early in Ethiopia Level 10/11

  hhu-adam/Robo#193 · Filter by author ByteEater-pl opened on Oct 6, 2026

• Cannot use 1 as matrix in Ethiopia Level 9 / 11

  hhu-adam/Robo#192 · Filter by author ByteEater-pl opened on Oct 6, 2026

• Simple theorem missing from Ethiopia Level 9 / 11

  hhu-adam/Robo#191 · Filter by author ByteEater-pl opened on Oct 6, 2026
  1

• Hint too magical in Ethiopia Level 9 / 11

  hhu-adam/Robo#190 · Filter by author ByteEater-pl opened on Oct 6, 2026

• Tactics rw and apply don't work when they should in Ethiopia Level 9 / 11

  hhu-adam/Robo#189 · Filter by author ByteEater-pl opened on Oct 6, 2026

• Surprising subgoal Fin n in Ethiopia Level 7 / 11

  hhu-adam/Robo#188 · Filter by author ByteEater-pl opened on Oct 4, 2026

• Missing x in hint in Vieta Level 10 / 10

  hhu-adam/Robo#187 · Filter by author ByteEater-pl opened on Oct 3, 2026

• Pressing enter when cursor is at non-final token boundary results in space insertion

  hhu-adam/Robo#186 · Filter by author ByteEater-pl opened on Oct 3, 2026

• Name automatically shadowed in Euclid Level 3 / 4

  hhu-adam/Robo#185 · Filter by author ByteEater-pl opened on Oct 2, 2026

• Hint uses fixed name in Euclid Level 3 / 4

  hhu-adam/Robo#184 · Filter by author ByteEater-pl opened on Oct 2, 2026

• No instruction how to compose ∈

  hhu-adam/Robo#183 · Filter by author ByteEater-pl opened on Oct 2, 2026
  2

• Why is toFinset in Theorems? (Euclid Level 3 / 4)

  hhu-adam/Robo#182 · Filter by author ByteEater-pl opened on Oct 2, 2026

• Unexpected result of obtain with nested pattern in Euclid Level 2 / 4

  hhu-adam/Robo#181 · Filter by author ByteEater-pl opened on Oct 2, 2026

• Weirdness in Euclid Level 1 / 4

  hhu-adam/Robo#180 · Filter by author ByteEater-pl opened on Oct 2, 2026
  1

• Wrong result of rw at *

  hhu-adam/Robo#179 · Filter by author ByteEater-pl opened on Oct 2, 2026

• Pattern for rw occurs in Prado Level 3 / 10, but rewriting denied

  hhu-adam/Robo#178 · Filter by author ByteEater-pl opened on Oct 2, 2026

• Instructions for composing ∣ misleading

  hhu-adam/Robo#177 · Filter by author ByteEater-pl opened on Oct 2, 2026

• Hint leads to error in Babylon Level 7 / 9

  hhu-adam/Robo#176 · Filter by author ByteEater-pl opened on Oct 1, 2026

• Occurrence for rw clearly present, yet error appears

  hhu-adam/Robo#175 · Filter by author ByteEater-pl opened on Oct 1, 2026
  1

• Two theorems named subset_iff in Level 10 / 10

  hhu-adam/Robo#174 · Filter by author ByteEater-pl opened on Oct 1, 2026

• Hint leads to variable shadowing in Level 9 / 10

  hhu-adam/Robo#173 · Filter by author ByteEater-pl opened on Oct 1, 2026

• Luna lv.3 suggests apply lt_trichotomy which can't actually be used

  hhu-adam/Robo#164 · Filter by author magistau opened on Jul 28, 2026

• Samarkand can be solved trivially by self-apply

  hhu-adam/Robo#145 · Filter by author Marti2203 opened on Jul 2, 2026
  2

• Unable to run the game locally

  hhu-adam/Robo#132 · Filter by author sharmaeklavya2 opened on Jun 19, 2026
  5