Alex Kontorovich - Teaching Real Analysis as a Video Game

Stream: Lean Together 2026

[Rémy Degenne]

Discussion topic for the talk.

[Alex Kontorovich]

In case anyone wants them, here are the slides:
2026LeanTogetherKontorovich.pdf

[Jared green]

at 3.2, the point where bound should be used, it doesnt work.

[Alex Kontorovich]

Sorry, can you be more specific? Maybe screen shot the situation? Thanks!

[Jared green]

image.png

[Edward van de Meent]

i think you should be using <= here rather than <? or you're missing a +1

[Jared green]

the +1 i dont think should be necessary

[Edward van de Meent]

but then the have isn't true? take epsilon equal to 1/2, then the inequality becomes 2 < 2, no?

[Edward van de Meent]

from the docs:

⌈a⌉₊ is the least natural n such that a ≤ n

so you can't conclude that there is a strict inequality.

[Jared green]

image.png

[Kim Morrison]

@Jared green, please don't post screen shots without explaining context and what it is you want explained.

[Jared green]

i wanted to know why bound was failing. i have already gotten past it now.

[Patrick Massot]

Note the conversation I was having with Alex after his talk continues at #Lean for teaching > Real analysis @ 💬.