• All Packages
  • Criteria
    • All Packages
    • Criteria
  • Readme
  • Versions (1)
  • Dependencies (11)

AlexKontorovichGame

RealAnalysisGame

METADATA

  • Apache 2.0
  • a month ago
    Last updated on May 22, 2026 at 8:28:12PM
  • 62 stars

LEAN

  • Commit 930c383 fails to build on leanprover/lean4:v4.26.0
    v4.26.0
  • Commit 26963c3 builds on the old leanprover/lean4:v4.23.0-rc2
    v4.23.0-rc2
  • Commit 3f108f7 builds on the old leanprover/lean4:v4.22.0 after lake update
    v4.22.0
  • 22 more

HOMEPAGE

adam.math.hhu.de/#/g/AlexKontorovich/RealAnalysisGame

REPOSITORY

AlexKontorovich/RealAnalysisGame

Real Analysis, The Game

Note that this is v0.1. Currently in progress (in a separate repo) is v1.0. Please continue to post Issues here, so we make sure to address them in the next version. But we're not currently maintaining v0.1. Thank you!

This is a game for lean4game.

The documentation about how to use this are at the lean4game repository:

  • Creating a new game
    • Updating an existing game
    • Running a game locally

Get Started

  • Install
  • Learn
  • Community
  • Reservoir

Documentation

  • Language reference
  • Lean API
  • Use cases
  • Cite Lean

Resources

  • Lean playground
  • VS Code extension
  • Loogle
  • Mathlib

FRO

  • Mission
  • Team
  • Roadmap
  • Contact

Policies

  • Privacy Policy
  • Terms of Use
© 2025 Lean FRO. All rights reserved.