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@v4
+      - uses: leanprover/lean-action@v1

.gitignore

@@ -0,0 +1 @@
+/.lake

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

KineticTheoryOfGasesLean/Basic.lean

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

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.

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"

lean-toolchain

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