lakefile.toml

name = "GQ2"
defaultTargets = ["GQ2"]

[leanOptions]
pp.unicode.fun = true
autoImplicit = false
relaxedAutoImplicit = false

# Dev tooling (NOT imported by GQ2): the Lean Atlas dependency-graph viewer.
# Pinned at the commit verified to build under this project's v4.31.0-rc2 toolchain.
# Has no shared transitive deps, so it does not affect Mathlib's pin precedence.
[[require]]
name = "lean-atlas"
scope = "NyxFoundation"
git = "https://github.com/NyxFoundation/lean-atlas"
rev = "3a81e194db0e6c41a2a8c5286f9e1b4962c3866a"

# `require mathlib` last so Mathlib's pinned versions of shared transitive
# dependencies (proofwidgets, batteries, …) take precedence over those of the
# other requires.  Pinned at ec410d2 (2026-06-12) for reproducibility.
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "ec410d23dfa4e7540d4663405b5e0dc71f3c3363"

[[lean_lib]]
name = "GQ2"

# Comparator (leanprover/comparator) verification pair for the main theorem;
# see comparator-config.json and formalization.yaml.
[[lean_lib]]
name = "Challenge"

[[lean_lib]]
name = "Solution"