home > research > lean4-4.26.0-freebsd-15 > index (2026-02-06)

Lean 4.26.0 on FreeBSD 15.0-RELEASE: Parity Differential Proof

Table of Contents

1. Overview

This document records the attempt to build the formal proof from arXiv:2602.03722 ("Parity of k-differentials in genus zero and one") on FreeBSD 15.0-RELEASE.

The proof requires Lean 4.26.0 specifically, which creates toolchain challenges on FreeBSD.

1.1. Paper Summary

  • Title: Parity of k-differentials in genus zero and one
  • Authors: Evan Chen, Kenny Lau, Ken Ono, Jujian Zhang
  • Repository: AxiomMath/parity-differential
  • Key Result: Determines spin parity of k-differentials with prescribed zero/pole orders
  • Proof Method: Formalized in Lean 4.26.0 with Mathlib, generated by AxiomProver

1.2. Version Requirements

Component Required FreeBSD pkg Available Notes
Lean 4.26.0 4.25.2 / 4.27.0-pre Version mismatch
Mathlib v4.26.0 N/A (built from src) Must match Lean version
elan Any working 4.1.2 (broken) Panics on FreeBSD

2. System Information

uname -a

FreeBSD nexus 15.0-RELEASE FreeBSD 15.0-RELEASE releng/15.0-n280995-7aedc8de6446 GENERIC amd64

lean --version
lake --version

Lean (version 4.27.0-pre, x86_64-unknown-freebsd15.0, Release)
Lake version 5.0.0-src (Lean version 4.27.0, commit )

3. The Proof

3.1. Problem Statement

For odd k >= 3, m = (k-1)/2, and n coprime to both k and (k+1):

Define Nk(n) as the count of pairs (b1, b2) in N x N such that:

  1. 1 <= b1 <= m
  2. 1 <= b2 <= m
  3. b1 + b2 >= m + 1
  4. b2 ≡ n * b1 (mod k)

Define Fk(a) = sum from i=1 to m of floor((a*i + m)/k)

Theorem: Nk(n) = Fk(n+1) - Fk(n)

3.2. Lean Formalization

The proof is in two files:

3.2.1. problem.lean (Statement)

def countingFunctionN (k : ℕ) (n : ℕ) : ℕ :=
  let m := (k - 1) / 2
  Finset.card (Finset.filter
    (fun p : ℕ × ℕ => m + 1 ≤ p.1 + p.2 ∧ p.2 % k = (n * p.1) % k)
    (Finset.Icc 1 m ×ˢ Finset.Icc 1 m))

def floorSumF (k : ℕ) (a : ℕ) : ℕ :=
  let m := (k - 1) / 2
  ∑ i ∈ Finset.Icc 1 m, (a * i + m) / k

theorem main_theorem (k : ℕ) (n : ℕ)
    (hk_ge : 3 ≤ k)
    (hk_odd : Odd k)
    (hn_coprime : Nat.Coprime n k)
    (hn1_coprime : Nat.Coprime (n + 1) k) :
    (countingFunctionN k n : ℤ) = (floorSumF k (n + 1) : ℤ) - (floorSumF k n : ℤ) := by
  sorry

3.2.2. solution.lean (Complete Proof)

The solution file contains 149 lines of Lean code with a complete proof (no sorry).

Key lemmas include:

  • two_mul_m_eq: 2 * ((k-1)/2) = k - 1 for odd k
  • div_of_succ_mul: Floor division decomposition
  • floor_term_eq_indicator: Converts floor terms to indicator functions
  • countingN_as_sum_over_i: Rewrites counting function as sum
  • floorSum_diff_eq_sum: Rewrites floor sum difference

4. Toolchain Issues on FreeBSD

4.1. Issue 1: elan 4.1.2 Package Bug

The FreeBSD elan package (version 4.1.2) panics on toolchain operations: 

elan toolchain install leanprover/lean4:v4.26.0

thread 'main' (844744) panicked at src/elan-dist/src/manifestation.rs:90:13:
internal error: entered unreachable code

4.2. Issue 2: lean4 Package Version Mismatch

The FreeBSD lean4 package provides version 4.25.2 (older than required 4.26.0), but the binary reports 4.27.0-pre: 

pkg info lean4 | grep -E "Name|Version"

Name           : lean4
Version        : 4.25.2.20251201

4.3. Issue 3: Mathlib Build Failures

Attempting to build with system Lean 4.27.0-pre fails due to API changes: 

error: Cache/Requests.lean:95:37: Invalid field `containsSubstr`:
  The environment does not contain `String.Slice.containsSubstr`

The String.trim → String.Slice API change between 4.26.0 and 4.27.0 breaks Mathlib's cache tool.

5. Attempted Workarounds

5.1. 1. Linux Binary Compatibility

FreeBSD has Linux binary compatibility enabled: 

kldstat | grep linux
ls /compat/linux | head -3

Lean 4.26.0 Linux binaries could potentially work but require additional setup.

5.2. 2. Building elan from Source

Requires Rust/cargo: 

ghq get github.com/leanprover/elan
cd $(ghq root)/github.com/leanprover/elan
cargo build --release

5.3. 3. GitHub Codespaces

The project builds successfully on GitHub Actions (ubuntu-latest): 

gh codespace create -R AxiomMath/parity-differential

5.4. 4. Building Lean from Source

ghq get github.com/leanprover/lean4
cd $(ghq root)/github.com/leanprover/lean4
git checkout v4.26.0
# Build instructions...

6. CI Verification

The proof is verified via GitHub Actions: 

name: Lean

on:
  push:
    branches: ["main"]
  workflow_dispatch:

jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: leanprover/lean-action@v1

Latest run: Success (2m22s) - 2026-02-05

The lean-action reads lean-toolchain file and installs the correct version via elan.

7. Required Versions for the Proof

From the repository:

File Content
lean-toolchain leanprover/lean4:v4.26.0
lakefile.toml mathlib rev = "v4.26.0"

8. Successful Workaround: GitHub Codespaces

Since FreeBSD toolchain issues block local verification, the recommended approach is using GitHub Codespaces.

8.1. Setup

# Ensure codespace scope
gh auth refresh -h github.com -s codespace

# Create codespace with sufficient resources
gh codespace create -R aygp-dr/parity-differential -m basicLinux32gb

8.2. Verification Steps

# SSH into codespace
gh codespace ssh -c <codespace-name>

# Install elan (works on Linux)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
source ~/.elan/env

# Build the proof
cd /workspaces/parity-differential
lake build

8.3. Timing (2026-02-06)

Operation Duration
Codespace creation ~30s
elan installation ~5s
Lean 4.26.0 toolchain download ~10s
Mathlib dependencies clone ~30s
Full mathlib build ~15-20 min
ParityDifferential build ~5s
Total (cold start) ~20 min

8.4. Makefile Target

The repository includes a Makefile for convenience: 

codespace: ## Create a GitHub Codespace for verification
        gh auth refresh -h github.com -s codespace
        gh codespace create -R $(REPO) -m $(CODESPACE_MACHINE)

Usage: gmake codespace

8.5. Cost Considerations

  • Machine type: basicLinux32gb (4-core, 16GB RAM, 32GB storage)
  • Build uses significant CPU during mathlib compilation
  • Storage includes mathlib cache after first build
  • Codespace can be stopped/started to preserve state

9. Next Steps

  1. [X] Build elan from source with Rust (works but same bug)
  2. [ ] Patch elan to support FreeBSD
  3. [X] Verify proof via GitHub Codespaces
  4. [ ] Build Lean 4.26.0 from source on FreeBSD

10. Comparison: FreeBSD Lean Versions

Version FreeBSD Status Notes
4.23.0 14.3 Working procfs required
4.25.2 15.0 pkg available Older than 4.26.0 requirement
4.26.0 15.0 Not available Required for parity-differential
4.27.0 15.0 pkg (4.25.2) Binary reports 4.27.0-pre, broken

11. References

12. Reproduction Attempts

12.1. Attempt 1: FreeBSD pkg elan (Failed)

$ pkg install elan
$ elan toolchain install leanprover/lean4:v4.26.0
thread 'main' panicked at src/elan-dist/src/manifestation.rs:90:13:
internal error: entered unreachable code

Root cause: elan doesn't support FreeBSD as a target OS (line 90 only checks for windows/linux/macos).

12.2. Attempt 2: Build elan from source (Failed)

ghq get github.com/leanprover/elan
git -C ~/ghq/github.com/leanprover/elan checkout v4.1.2
cargo build --release --manifest-path ~/ghq/github.com/leanprover/elan/Cargo.toml
# Build succeeds in 9m 30s
~/.elan/bin/elan-init -y --no-modify-path
~/.elan/bin/elan toolchain install leanprover/lean4:v4.26.0
# Same panic - bug is in source, not just pkg

Root cause: Same code path as pkg - FreeBSD not supported.

12.3. Attempt 3: Linux binary with compat layer (Partial success)

# Download Linux binaries
mkdir -p ~/.local/lean-4.26.0
curl -L "https://github.com/leanprover/lean4/releases/download/v4.26.0/lean-4.26.0-linux.tar.zst" \
  -o ~/.local/lean-4.26.0/lean.tar.zst
zstd -d ~/.local/lean-4.26.0/lean.tar.zst -o ~/.local/lean-4.26.0/lean.tar
tar -xf ~/.local/lean-4.26.0/lean.tar -C ~/.local/lean-4.26.0/

# Verify lean works (via Linux compat)
~/.local/lean-4.26.0/lean-4.26.0-linux/bin/lean --version
# Output: Lean (version 4.26.0, x86_64-unknown-linux-gnu, ...)

Status: lean and lake binaries work, but bundled clang fails: 

/home/jwalsh/.local/lean-4.26.0/lean-4.26.0-linux/bin/clang: \
  /lib64/libm.so.6: version `GLIBC_2.29' not found

Root cause: FreeBSD's Linux compat layer provides older glibc than Lean's bundled clang requires.

12.4. Attempt 4: hydra.lan (FreeBSD 14.3)

ssh hydra.lan "sudo mount -t procfs proc /proc"  # Required for lean
ssh hydra.lan "lean --version"
# Lean (version 4.27.0-pre, x86_64-unknown-freebsd14.3, Release)

Status: Works but version 4.27.0-pre, not 4.26.0 required.

12.5. Attempt 5: GitHub Codespaces (Success)

# From FreeBSD host
gh codespace create -R aygp-dr/parity-differential -m basicLinux32gb
# Created: verbose-space-doodle-v6q5x4w5jvpg2w6v9

# SSH and build
gh codespace ssh -c verbose-space-doodle-v6q5x4w5jvpg2w6v9 -- \
  'curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y'

gh codespace ssh -c verbose-space-doodle-v6q5x4w5jvpg2w6v9 -- \
  'cd /workspaces/parity-differential && source ~/.elan/env && lake build'

Status: Success. Full mathlib build completes in ~20 minutes.

Output: 

info: downloading https://releases.lean-lang.org/lean4/v4.26.0/lean-4.26.0-linux.tar.zst
info: installing /home/codespace/.elan/toolchains/leanprover--lean4---v4.26.0
info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: mathlib: checking out revision '2df2f0150c275ad53cb3c90f7c98ec15a56a1a67'
...
✔ Built ParityDifferential.solution
✔ Built ParityDifferential.problem
✔ Built ParityDifferential

12.6. Summary Table

Machine OS Lean Available Required Status
nexus FreeBSD 15.0 4.27.0-pre 4.26.0 Version mismatch
nexus (linux) Linux compat 4.26.0 4.26.0 glibc too old
hydra.lan FreeBSD 14.3 4.27.0-pre 4.26.0 Version mismatch
GH Codespace Ubuntu (Linux) 4.26.0 4.26.0 SUCCESS

13. Version Discovery

13.1. Available Lean Versions

Source Version Notes
FreeBSD pkg (14.3) 4.25.2.20251201 Binary reports 4.27.0-pre
FreeBSD pkg (15.0) 4.25.2.20251201 Binary reports 4.27.0-pre
Linux binary 4.26.0 Works for lean, clang fails
elan (if worked) Any Not supported on FreeBSD

13.2. elan Tags

$ git -C ~/ghq/github.com/leanprover/elan tag | tail -5
v4.0.1
v4.1.0
v4.1.1
v4.1.2

13.3. Timing

Operation Time
elan build from source (FreeBSD) 9m 30s
Lean 4.26.0 download ~7s
Mathlib clone (failed on FreeBSD) ~1m
Codespace creation ~30s
elan install (codespace) ~5s
Mathlib full build (codespace) ~20 min
ParityDifferential build ~5s

14. Appendix: Full Diagnostic Output

echo "=== System ==="
uname -a
echo ""
echo "=== Packages ==="
pkg info lean4 elan 2>&1 | grep -E "Name|Version" || true
echo ""
echo "=== procfs ==="
mount | grep proc
echo ""
echo "=== Lean ==="
lean --version 2>&1 || echo "FAILED"
lake --version 2>&1 || echo "FAILED"

Author: Jason Walsh

j@wal.sh

Last Updated: 2026-02-06 20:49:08

build: 2026-04-17 18:35 | sha: 792b203