Skip to content

Commit 876f001

Browse files
phasetrclaude
phasetr
and
claude
committed
Initialize Lean 4 + mathlib project for Ising model formalization
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
0 parents  commit 876f001

10 files changed

Lines changed: 215 additions & 0 deletions

File tree

‎.github/workflows/create-release.yml‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
name: Create Release
2+
3+
on:
4+
push:
5+
branches:
6+
- 'main'
7+
- 'master'
8+
paths:
9+
- 'lean-toolchain'
10+
11+
jobs:
12+
lean-release-tag:
13+
name: Add Lean release tag
14+
runs-on: ubuntu-latest
15+
permissions:
16+
contents: write
17+
steps:
18+
- name: lean-release-tag action
19+
uses: leanprover-community/lean-release-tag@v1
20+
with:
21+
do-release: true
22+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

‎.github/workflows/lean_action_ci.yml‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
name: Lean Action CI
2+
3+
on:
4+
push:
5+
pull_request:
6+
workflow_dispatch:
7+
8+
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
9+
permissions:
10+
contents: read # Read access to repository contents
11+
pages: write # Write access to GitHub Pages
12+
id-token: write # Write access to ID tokens
13+
14+
jobs:
15+
build:
16+
runs-on: ubuntu-latest
17+
18+
steps:
19+
- uses: actions/checkout@v5
20+
- uses: leanprover/lean-action@v1
21+
- uses: leanprover-community/docgen-action@v1

‎.github/workflows/update.yml‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
name: Update Dependencies
2+
3+
on:
4+
# schedule: # Sets a schedule to trigger the workflow
5+
# - cron: "0 8 * * *" # Every day at 08:00 AM UTC (see https://docs.github.com/en/actions/writing-workflows/choosing-when-your-workflow-runs/events-that-trigger-workflows#schedule)
6+
workflow_dispatch: # Allows the workflow to be triggered manually via the GitHub interface
7+
8+
jobs:
9+
check-for-updates: # Determines which updates to apply.
10+
runs-on: ubuntu-latest
11+
outputs:
12+
is-update-available: ${{ steps.check-for-updates.outputs.is-update-available }}
13+
new-tags: ${{ steps.check-for-updates.outputs.new-tags }}
14+
steps:
15+
- name: Run the action
16+
id: check-for-updates
17+
uses: leanprover-community/mathlib-update-action@v1
18+
# START CONFIGURATION BLOCK 1
19+
# END CONFIGURATION BLOCK 1
20+
do-update: # Runs the upgrade, tests it, and makes a PR/issue/commit.
21+
runs-on: ubuntu-latest
22+
permissions:
23+
contents: write # Grants permission to push changes to the repository
24+
issues: write # Grants permission to create or update issues
25+
pull-requests: write # Grants permission to create or update pull requests
26+
needs: check-for-updates
27+
if: ${{ needs.check-for-updates.outputs.is-update-available == 'true' }}
28+
strategy: # Runs for each update discovered by the `check-for-updates` job.
29+
max-parallel: 1 # Ensures that the PRs/issues are created in order.
30+
matrix:
31+
tag: ${{ fromJSON(needs.check-for-updates.outputs.new-tags) }}
32+
steps:
33+
- name: Run the action
34+
id: update-the-repo
35+
uses: leanprover-community/mathlib-update-action/do-update@v1
36+
with:
37+
tag: ${{ matrix.tag }}
38+
# START CONFIGURATION BLOCK 2
39+
on_update_succeeds: pr # Create a pull request if the update succeeds
40+
on_update_fails: issue # Create an issue if the update fails
41+
# END CONFIGURATION BLOCK 2

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
/.lake

‎IsingModel.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
import IsingModel.Basic

‎IsingModel/Basic.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
def hello := "world"

‎README.md‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
# ising-model
2+
3+
A Lean 4 + mathlib project for formalizing theorems about the Ising model.
4+
5+
## Related projects and references
6+
7+
- [YaelDillies/gibbs-measure](https://github.com/YaelDillies/gibbs-measure) — Lean 4 formalization project on Gibbs measures
8+
- [leanprover-community/physlib](https://github.com/leanprover-community/physlib) — A physics library in Lean 4
9+
- Friedli, S. and Velenik, Y., *Statistical Mechanics of Lattice Systems: A Concrete Mathematical Introduction* — [De Gruyter](https://www.degruyterbrill.com/document/doi/10.1515/9783110250329/html)
10+
11+
## Learning resources
12+
13+
- [The Mechanics of Proof (Math 2001)](https://hrmacbeth.github.io/math2001/) by Heather Macbeth
14+
- [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/index.html)

‎lake-manifest.json‎

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
{"version": "1.1.0",
2+
"packagesDir": ".lake/packages",
3+
"packages":
4+
[{"url": "https://github.com/leanprover-community/mathlib4",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "leanprover-community",
8+
"rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95",
9+
"name": "mathlib",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "v4.29.0",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/leanprover-community/plausible",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "leanprover-community",
18+
"rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
19+
"name": "plausible",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "main",
22+
"inherited": true,
23+
"configFile": "lakefile.toml"},
24+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
25+
"type": "git",
26+
"subDir": null,
27+
"scope": "leanprover-community",
28+
"rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
29+
"name": "LeanSearchClient",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": "main",
32+
"inherited": true,
33+
"configFile": "lakefile.toml"},
34+
{"url": "https://github.com/leanprover-community/import-graph",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "leanprover-community",
38+
"rev": "48d5698bc464786347c1b0d859b18f938420f060",
39+
"name": "importGraph",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "main",
42+
"inherited": true,
43+
"configFile": "lakefile.toml"},
44+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "leanprover-community",
48+
"rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3",
49+
"name": "proofwidgets",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "v0.0.95",
52+
"inherited": true,
53+
"configFile": "lakefile.lean"},
54+
{"url": "https://github.com/leanprover-community/aesop",
55+
"type": "git",
56+
"subDir": null,
57+
"scope": "leanprover-community",
58+
"rev": "7152850e7b216a0d409701617721b6e469d34bf6",
59+
"name": "aesop",
60+
"manifestFile": "lake-manifest.json",
61+
"inputRev": "master",
62+
"inherited": true,
63+
"configFile": "lakefile.toml"},
64+
{"url": "https://github.com/leanprover-community/quote4",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "leanprover-community",
68+
"rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
69+
"name": "Qq",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "master",
72+
"inherited": true,
73+
"configFile": "lakefile.toml"},
74+
{"url": "https://github.com/leanprover-community/batteries",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "756e3321fd3b02a85ffda19fef789916223e578c",
79+
"name": "batteries",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "main",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover/lean4-cli",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover",
88+
"rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
89+
"name": "Cli",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "v4.29.0",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"}],
94+
"name": "«ising-model»",
95+
"lakeDir": ".lake"}

‎lakefile.toml‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
name = "ising-model"
2+
version = "0.1.0"
3+
keywords = ["math"]
4+
defaultTargets = ["IsingModel"]
5+
6+
[leanOptions]
7+
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
8+
relaxedAutoImplicit = false
9+
weak.linter.mathlibStandardSet = true
10+
maxSynthPendingDepth = 3
11+
12+
[[require]]
13+
name = "mathlib"
14+
scope = "leanprover-community"
15+
rev = "v4.29.0"
16+
17+
[[lean_lib]]
18+
name = "IsingModel"

‎lean-toolchain‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
leanprover/lean4:v4.29.0

0 commit comments

Comments
 (0)