From 12b397590bb8e9f0e3b8fda66fa1995bb50b577d Mon Sep 17 00:00:00 2001
From: Dibyashanu Pati <>
Date: Wed, 2 Apr 2025 04:06:06 +0530
Subject: [PATCH] initial commit

---
 .github/workflows/lean_action_ci.yml | 14 ++++++++++++++
 .gitignore                           |  1 +
 KineticTheoryOfGasesLean.lean        |  3 +++
 KineticTheoryOfGasesLean/Basic.lean  |  1 +
 README.md                            |  3 +++
 lakefile.toml                        | 15 +++++++++++++++
 lean-toolchain                       |  1 +
 7 files changed, 38 insertions(+)
 create mode 100644 .github/workflows/lean_action_ci.yml
 create mode 100644 .gitignore
 create mode 100644 KineticTheoryOfGasesLean.lean
 create mode 100644 KineticTheoryOfGasesLean/Basic.lean
 create mode 100644 README.md
 create mode 100644 lakefile.toml
 create mode 100644 lean-toolchain

diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
new file mode 100644
index 0000000..09cd4ca
--- /dev/null
+++ b/.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@v4
+      - uses: leanprover/lean-action@v1
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..bfb30ec
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/KineticTheoryOfGasesLean.lean b/KineticTheoryOfGasesLean.lean
new file mode 100644
index 0000000..4eddf8f
--- /dev/null
+++ b/KineticTheoryOfGasesLean.lean
@@ -0,0 +1,3 @@
+-- This module serves as the root of the `KineticTheoryOfGasesLean` library.
+-- Import modules here that should be built as part of the library.
+import KineticTheoryOfGasesLean.Basic
diff --git a/KineticTheoryOfGasesLean/Basic.lean b/KineticTheoryOfGasesLean/Basic.lean
new file mode 100644
index 0000000..99415d9
--- /dev/null
+++ b/KineticTheoryOfGasesLean/Basic.lean
@@ -0,0 +1 @@
+def hello := "world"
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..23a7294
--- /dev/null
+++ b/README.md
@@ -0,0 +1,3 @@
+# Kinetic_Theory_of_Gases_Lean
+
+The aim of this project is to formalize the Kinetic Theory of Gases in Lean4.
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..5958cf6
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,15 @@
+name = "Kinetic_Theory_of_Gases_Lean"
+version = "0.1.0"
+keywords = ["math"]
+defaultTargets = ["KineticTheoryOfGasesLean"]
+
+[leanOptions]
+pp.unicode.fun = true # pretty-prints `fun a ↦ b`
+autoImplicit = false
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+
+[[lean_lib]]
+name = "KineticTheoryOfGasesLean"
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..b2153cd
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.18.0