Order, lattices, ordered algebraic structures
The Lean Pool projects whose card's first MSC2020 code is in class 06, “Order, lattices, ordered algebraic structures”: 4 articles, one per card.
TheoremAnalysis of Boolean functions in Lean#
Walsh-Fourier analysis on Boolean functions, including Arrow's theorem and BLR linearity testing.
Quoted from the card LeanPool/projects/lean-booleanfun.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
LeanPool.LeanBooleanfun.BooleanFun.BV.dictator_of_condorcet_and_unanimous(theorem; a main declaration), declared in LeanPool/LeanBooleanfun/Arrow.lean, line 271: “Arrow's theorem for two-candidate Boolean voting rules.”
Project
- Authors: Joris Roos.
- Source: doi:10.1017/CBO9781139814782, arXiv:2105.10386.
- Project repository: roos-j/lean-booleanfun.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 06E30, 42C10, 91B14.
- In Lean Pool: LeanPool/LeanBooleanfun, from the card LeanPool/projects/lean-booleanfun.yaml.
Sources
TheoremConway refinement for omnific integers#
Proves multiplicative refinement for omnific integers: every equality ab = cd admits a two-by-two factor refinement. Develops factorization and refinement of generalized power-series integer parts and connects these to surreal-number and standalone Mathlib formulations.
Quoted from the card LeanPool/projects/conway-refinement.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
ConwayRefinement.Palomar.conwayRefinement(theorem; a main declaration), declared in LeanPool/ConwayRefinement/Solution.lean, line 23: “If four omnific integers satisfy ab = cd, there are omnific integers e, f, g, h with a = ef, b = gh, c = eg, and d = fh, including degenerate cases.”
Project
- Authors: Dan Abramov.
- Project repository: gaearon/conway-refinement, at commit 264445c9.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 06A05, 13F25.
- In Lean Pool: LeanPool/ConwayRefinement, from the card LeanPool/projects/conway-refinement.yaml.
Sources
TheoremDisproof of the Aharoni-Korman Conjecture#
Formalizes Hollom's counterexample to the Aharoni-Korman fishbone conjecture for partially ordered sets.
Quoted from the card LeanPool/projects/aharonikorman.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
LeanPool.AharoniKorman.aharoni_korman_false(theorem; a main declaration), declared in LeanPool/AharoniKorman/Counterexample.lean, line 1244: “Proves that not every partially ordered set has either an infinite antichain or a chain meeting every antichain in a partition.”
Project
- Authors: Bhavik Mehta.
- Source: doi:10.1007/BF00383948, arXiv:2411.16844.
- Project repository: b-mehta/AharoniKorman.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 06A06, 06A07.
- In Lean Pool: LeanPool/AharoniKorman, from the card LeanPool/projects/aharonikorman.yaml.
Sources
TheoremSensitivity Conjecture: sqrt(deg) <= sensitivity#
Formalizes the quantitative Nisan-Szegedy/Huang sensitivity theorem for Boolean functions.
Quoted from the card LeanPool/projects/sensitivity.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
LeanPoolSensitivity.sensitivity_ge_sqrt_degree(theorem; a main declaration), declared in LeanPool/Sensitivity/Main.lean, line 46: “Proves that the square root of multilinear degree is bounded above by sensitivity.”LeanPoolSensitivity.degree_le_sensitivity_sq(theorem), declared in LeanPool/Sensitivity/Consequences.lean, line 32: “Derives the degree bound by the square of sensitivity.”
Project
- Authors: Samuel Schlesinger.
- Source: doi:10.4007/annals.2019.190.3.6, arXiv:1907.00847.
- Project repository: SamuelSchlesinger/sensitivity-conjecture.
- Provenance: mix, which in Lean Pool's terms means people and AI “both contributed substantially” to its Lean proofs.
- License: Apache-2.0.
- MSC2020: 06E30, 68Q17.
- In Lean Pool: LeanPool/Sensitivity, from the card LeanPool/projects/sensitivity.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.