initial commit

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v5
+      - uses: leanprover/lean-action@v1

.gitignore

@@ -0,0 +1,37 @@
+# from https://github.com/leanprover/lean4/blob/master/.gitignore
+*~
+\#*
+.#*
+.lake
+lake-manifest.json
+/build
+/src/lakefile.toml
+/lakefile.toml
+GPATH
+GRTAGS
+GSYMS
+GTAGS
+.projectile
+.lean_options
+.vs
+compile_commands.json
+*.idea
+tasks.json
+settings.json
+!.claude/settings.json
+.gdb_history
+.vscode/*
+!.vscode/settings.json
+!.vscode/tasks.json
+!.vscode/extensions.json
+script/__pycache__
+*.produced.out
+CMakeSettings.json
+CppProperties.json
+result
+fwIn.txt
+fwOut.txt
+wdErr.txt
+wdIn.txt
+wdOut.txt
+.claude/worktrees/

Main.lean

@@ -0,0 +1,4 @@
+import ZeroToLean
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"

README.md

@@ -1,2 +1,11 @@
-# ZeroToLean
+#### 2026-07-21
-My journey with Lean4. Starting with _Theorem Proving in Lean 4_ during the summer and a math bachelor @EPFL
+
+Note : I don't probably realize the amount of work. Hence, I might stop this project at some point.
+
+I will start at bachelor in mathematics at [EPFL](epfl.ch) and I set to myself the goal to formalize most of proofs and theorems seen in class to learn Lean4 and understand in depth the theorems I will see.
+
+See Index.md for a list of theorems, lemmas and corralary and the small set of proofs imported from mathlib (I don't want to derive everything from ZFC so I'll base myself on some mathlib proofs).
+
+To learn Lean and prepare myself, I will read this month _Theorem Proving in Lean 4_.
+
+I will try to continusly update this README.md tracking my advance.

ZeroToLean.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `ZeroToLean` library.
+-- Import modules here that should be built as part of the library.
+import ZeroToLean.Basic

ZeroToLean/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.33.0-rc1