LinearAlgebraGame/Game.lean at main · blfang/LinearAlgebraGame · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
-- Basic game configuration without levels for initial setup test
import GameServer.Commands
import Game.Levels.TutorialWorld
import Game.Levels.VectorSpaceWorld
import Game.Levels.LinearIndependenceSpanWorld
import Game.Levels.LinearMapsWorld
import Game.Levels.InnerProductWorld

Title "Linear Algebra Game"
Introduction
"
# Welcome to the Linear Algebra Game!

This game works as a learning tool for linear algebra,
based on the textbook \"Linear Algebra Done Right\" by Sheldon Axler. It also serves as an
introduction to Lean 4, a proof assistant that provides an environment to encode proofs formally.

Proofs in Lean are written in precise syntax, using tactics and theorems, and can be algorithmically
checked for correctness by a computer.

This game covers many areas of linear algebra, including vector spaces, linear independence, bases,
linear mappings, and isomorphisms.

To start, click on \"Tutorial World\"
"

Info "
*Game version: 1.0*

## Progress saving

The game stores your progress in your local browser storage.
If you delete it, your progress will be lost!

Warning: In most browsers, deleting cookies will also clear the local storage
(or \"local site data\"). Make sure to download your game progress first!

## Issues and Feedback

If you encounter any bugs, have suggestions, or want to report issues,
please file them at: https://github.com/ZRTMRH/LinearAlgebraGame/issues

## Credits

* **Team:** Huiyu Chen, Adam Kern, Justin Morrill, and Letian Yang
* **Project Manager:** Daniel Zhou
* **Project Leader:** Professor Colleen Robles
* **2023 Lean 3 Version:** Yannan Bai, Annapurna Bhattacharya, Chun-Hsien Hsu, Stavan Jain, Kurt Ma, Ricardo Prado Cunha, Anoushka Sinha (Project Manager: Chun-Hsien Hsu)
* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot
* **Inspiration:** Kevin Buzzard's Natural Number Game (https://adam.math.hhu.de/#/g/leanprover-community/nng4)
* **Cover Image:** Daniel Zhou, Nina Ma
"

Languages "English"
CaptionShort "Linear Algebra Game"
CaptionLong "Learn linear algebra through interactive theorem proving in Lean 4. Prove famous results like the Cauchy-Schwarz inequality and work through vector spaces, linear independence, and inner products based on Axler's 'Linear Algebra Done Right'."
CoverImage "images/cover.png"

namespace LinearAlgebraGame

MakeGame

end LinearAlgebraGame