funlean.
A reading order for this chapter

The extremely literal judge

The prerequisites are included before the words that depend on them. Skip what you already know.

Start with step one → Return to the story

  1. Reading a Lean statement

    High school

    Separate the objects, their conditions, and the conclusion.

  2. Axioms and proof checking

    Proof level

    Inspect which foundational assumptions a theorem’s proof uses.

I’m lost · Help

Mika’s help desk

The extremely literal judge · A reading order for this chapter

One thing at a time

Start with the cake-scale story. You only need to read one small piece at a time. If you are in the Fermat story, start with Story depth, then the words listed before the chapter.

In simpler words

You do not need to know Lean, symbols or university mathematics to begin. Definitions come first in the small stories.

A small clue

Look at the small example before the general formula. Ask what changed and what stayed the same.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →