Lean videogame

Demo: Prove the theorem to make the muppets sing.

  • Generalize muppets to fun videos.

  • Specialize to videos with famous scientists in them. Professors giving hints, reliving the experience of discovering the proof, etc.

  • Evergreen videos;

Demo: Prove the theorem to change the scene.

Smoothly transition between scenes when the proof is complete. One of the features of mnemonic videos in the article.

For an interesting enough film, would people learn the theorems to keep watching:

Edward Witten in a Godfather-like scene. The film opens with Witten petting a cat in a study. Someone’s wedding going on in the background. Witten is discussing a paper’s proof with another famous scientisit.

Demo: A proof that beeps.

  • Use the music to convey information about the steps of the proof:

    • Play a dramatic note at important have H1 : {} blocks;

    • When certain useful external theorems or lemmas are used, play music to convey a sense of, “aha, nice, you figured this piece out.”

    • Play a note to indicate a nearby finale (see examples in Crash Bandicoot and Matrix: The path of Neo).

      • Need a system to predict how far someone is from proving something.

        • Simple example: The system checks if the proof can be finished using the finish tactic.

        • Another example: A Machimatician works out the proof from where the player stands. Decides how far the player is from the end.

  • A complete proof then forms a song. And nice songs are easily remembered; You listen to them until they stick in your head. Use music and comedy to 𓋴𓃀𓇼𓏜 efficiently. Perhaps when the learners have done many proofs that map to songs, they will develop a kind of musical intuiton when approaching theorem proving. Will they hear math in their head?

  • Suppose each theorem had a “song” associated with it. The song depends on the proof of the theorem. Would it be cool if each time the theorem is used, the theorem’s song plays in the background?

  • Hire mathematicians to ask them how they feel during the proof. Hire a band to help you convey the feeling in music. Write project descriptions;

  • Mozilla’s webaudio API to programmatically play keyboard notes.

Can you put the demos on something similar to Lean repl;

References