NOTICE

Lean Pool
=========

Copyright the Lean Pool contributors and the respective project authors.

Lean Pool is licensed under the Apache License, Version 2.0. See the LICENSE
file for the full license text.

Lean Pool is an aggregation of third-party Lean 4 formalizations. Each project
under LeanPool/ is the work of its original authors, who retain copyright as
recorded in the per-file headers and in LeanPool/projects.yml. This NOTICE file
records, for every pooled project, the upstream repository it was imported from
and the license under which it was originally published.

This file is generated by python/lean_pool/notice.py from LeanPool/projects.yml
and NOTICE.extra.yml. Do not edit it by hand -- edit those inputs instead.


--------------------------------------------------------------------------------
Projects originally licensed under the Apache License, Version 2.0
--------------------------------------------------------------------------------

These projects were imported from repositories already licensed under the
Apache License, Version 2.0, and are redistributed here under the same license.

  LeanPool/ABCExceptions             https://github.com/b-mehta/ABC-Exceptions
  LeanPool/AFormalizationOfBorelDeterminacyInLean
                                     https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean
  LeanPool/AharoniKorman             https://github.com/b-mehta/AharoniKorman
  LeanPool/AndersonConjecture        https://github.com/frenzymath/Anderson-Conjecture
  LeanPool/Apportionment             https://github.com/mdbrnowski/apportionmentlib
  LeanPool/ArchonFirstProofResults   https://github.com/frenzymath/Archon-FirstProof-Results
  LeanPool/BannaiBannaiStanton       https://github.com/AntoineduFresne/Bannai-Bannai-Stanton_Theorem
  LeanPool/BooleanIsoperimetry       https://github.com/AlexeyMilovanov/BooleanIsoperimetry
  LeanPool/BrauerGroupNew            https://github.com/Whysoserioushah/BrauerGroup
  LeanPool/BruhatTits                https://github.com/chrisflav/bruhat-tits
  LeanPool/Burkholder                https://github.com/SmaniaD/Burkholder
  LeanPool/CencovPetz                https://github.com/abenenson/cencov-petz
  LeanPool/ChannelCapacity           https://github.com/abenenson/channel-capacity
  LeanPool/Chudnovsky                https://github.com/ldct/lean-eval-chudnovsky
  LeanPool/CircuitComplexity         https://github.com/SamuelSchlesinger/circuit-complexity
  LeanPool/Circuitlib                https://github.com/matthunz/circuitlib
  LeanPool/ClassificationOfSurfaces  https://github.com/mccorvie/classification-of-surfaces
  LeanPool/CompactSpectral           https://github.com/abenenson/compact-spectral
  LeanPool/CompositionAlgebras       https://github.com/ehrlich-b/composition-algebras
  LeanPool/Computability             https://github.com/tannerduve/computability
  LeanPool/ComputableReal            https://github.com/Timeroot/computableReal
  LeanPool/ConnesKreimer             https://github.com/karlesmarin/connes-kreimer-lean
  LeanPool/ConnesRigidity            https://github.com/utensil/connes-rigidity
  LeanPool/CramerWold                https://github.com/Lemmy00/lean-pool
  LeanPool/CriticalPortraits         https://github.com/no-way-labs/lean-critical-portraits
  LeanPool/DemazureOperatorsLean     https://github.com/bolito2/DemazureOperatorsLean
  LeanPool/DemazureProduct           https://github.com/npflueger/demazure
  LeanPool/Desargues                 https://github.com/oneofvalts/desargues
  LeanPool/DistanceGeometry          https://github.com/lyfar/distance-geometry-lean
  LeanPool/DomainTheory              https://github.com/catskillsresearch/domain_theory
  LeanPool/Duality                   https://github.com/madvorak/duality
  LeanPool/EcTateLean                https://github.com/KisaraBlue/ec-tate-lean
  LeanPool/Egrs75                    https://github.com/lyfar/egrs75-lean
  LeanPool/Erdos1196                 https://github.com/math-inc/Erdos1196
  LeanPool/Erdos132ConvexK3          https://github.com/lyfar/erdos-132-convex-k3-lean
  LeanPool/Erdos132N14               https://github.com/lyfar/erdos-132-moment-obstruction-lean
  LeanPool/Erdos132ThreeChain        https://github.com/lyfar/lean-pool
  LeanPool/Erdos137                  https://github.com/scottdhughes/erdos137
  LeanPool/Erdos346                  https://github.com/KitaKen1/erdos346-ratio-limit-lean
  LeanPool/Erdos367                  https://github.com/scottdhughes/erdos367
  LeanPool/Erdos403                  https://github.com/gotrevor/erdos-403
  LeanPool/Erdos81PaperIContrib      https://github.com/jtraverso/erdos-81-chordal-clique-partitions
  LeanPool/Erdos81PaperIIIContrib    https://github.com/jtraverso/erdos-81-chordal-clique-partitions
  LeanPool/Erdos865                  https://github.com/mrricky22/erdos-865-lean
  LeanPool/Erdos97ConvexOctagon      https://github.com/lyfar/erdos-97-octagon-lean
  LeanPool/ErdosMoser                https://github.com/lyfar/erdos-moser-distinct-subset-sums-lean
  LeanPool/ErdosTuzaValtr            https://github.com/jcpaik/erdos-tuza-valtr
  LeanPool/EventStructures           https://github.com/vikraman/event-structures
  LeanPool/Feige                     https://github.com/pengzhang91/Feige
  LeanPool/Fineqs                    https://github.com/nasqret/fineqs
  LeanPool/FiniteGraphFundamentalGroup
                                     https://github.com/Arthur742Ramos/finite-graph-fundamental-group
  LeanPool/FiveEighthsTheorem        https://github.com/ldct/lean-monorepo
  LeanPool/Flean                     https://github.com/josephmckinsey/flean
  LeanPool/FltRegular                https://github.com/leanprover-community/flt-regular
  LeanPool/FoZfc                     https://github.com/ishiut/fo_zfc
  LeanPool/FormalLearningTheory      https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel
  LeanPool/FriezePatterns            https://github.com/Antoine-dSG/frieze_patterns
  LeanPool/FrontierMathOpenHypergraphs
                                     https://github.com/math-inc/FrontierMathOpen-Hypergraphs
  LeanPool/FundamentalInequality     https://github.com/linzialessandro/FundamentalInequality
  LeanPool/GKPCarry                  https://github.com/lyfar/gkp-carry-lean
  LeanPool/HadwigerNelsonBounds      https://github.com/lyfar/hadwiger-nelson-bounds-lean
  LeanPool/HansonWright              https://github.com/Lean-MoDS/StatsMLlib
  LeanPool/Incompleteness            https://github.com/FormalizedFormalLogic/Incompleteness
  LeanPool/IsTranscendentalPi        https://github.com/samuelborza/IsTranscendentalPi
  LeanPool/IsoGraph                  https://github.com/Timeroot/IsoGraph
  LeanPool/Isoperimetric             https://github.com/hojonathanho/isoperimetric
  LeanPool/JacobianDiffgeo           https://github.com/rkirov/jacobian-fable
  LeanPool/JohnsonLindenstraussLean  https://github.com/claytomode/johnson-lindenstrauss-lean
  LeanPool/KahnKalai                 https://github.com/dcposch/kahn-kalai-lean
  LeanPool/KasamiCyclicAdditive      https://github.com/dsm054/kasami_cyclic_additive
  LeanPool/KrafftSieve               https://github.com/ElNando888/KrafftSieve
  LeanPool/Lean4GlCoalgebras         https://github.com/mgignoux/lean4-gl-coalgebras
  LeanPool/LeanBooleanfun            https://github.com/roos-j/lean-booleanfun
  LeanPool/LeanComplexAnalysis       https://github.com/seb488/LeanComplexAnalysis
  LeanPool/LeanModelChecking         https://github.com/kuruczgy/lean-model-checking
  LeanPool/LeanModularForms          https://github.com/CBirkbeck/LeanModularForms
  LeanPool/LeanPolyABC               https://github.com/seewoo5/lean-poly-abc
  LeanPool/LeanQuantumAlg            https://github.com/QudeLeap/Lean-QuantumAlg
  LeanPool/LehmerE10                 https://github.com/dillon-11/lehmer-E10
  LeanPool/Lentil                    https://github.com/verse-lab/Lentil
  LeanPool/LocalComplexGeometry      https://github.com/BochaoKong/nullstellensatz
  LeanPool/LongGapsBetweenPrimes     https://github.com/openai/LongGapsBetweenPrimes
  LeanPool/LowDimSolvClassification  https://github.com/LieLean/LowDimSolvClassification
  LeanPool/MRiscX                    https://github.com/JulsDE/MRiscX
  LeanPool/MatchingLogic             https://github.com/eveil-labs/matching-logic-lean
  LeanPool/MinModulusUniqueMultisetSum
                                     https://github.com/jarfo/min-modulus
  LeanPool/MisereGames               https://github.com/t4ccer/misere-games
  LeanPool/Monlib4                   https://github.com/themathqueen/monlib4
  LeanPool/Monsky                    https://github.com/dhyan-aranha/Monsky
  LeanPool/MoserLatticeColorings     https://github.com/lyfar/moser-lattice-colorings-lean
  LeanPool/MulticolorTriangleRamsey  https://github.com/openai/ten-proofs
  LeanPool/Neukirch                  https://github.com/jjdishere/neukirch
  LeanPool/OSforGFF                  https://github.com/mrdouglasny/OSforGFF
  LeanPool/OddPrimeValuationDistribution
                                     https://github.com/lyfar/gkp-carry-lean
  LeanPool/Odlyzko                   https://github.com/ImperialCollegeLondon/FLT
  LeanPool/OrderPQ                   https://github.com/wupr/order-p-q
  LeanPool/PebblingLean              https://github.com/pachterlab/P_2026_2
  LeanPool/PentagonalNumberTheorem   https://github.com/wwylele/PentagonalNumberTheorem
  LeanPool/PermanentFormulaLowerBound
                                     https://github.com/openai/ten-proofs
  LeanPool/PhaseRetrieval            https://github.com/susannabertolini/PhaseRetrieval
  LeanPool/PoincareThreeBody         https://github.com/gersh/lean-pool
  LeanPool/PointwiseBirkhoff         https://github.com/lua-vr/pointwise-birkhoff
  LeanPool/Polylean                  https://github.com/siddhartha-gadgil/Polylean
  LeanPool/PolynomialMethodRestrictedSums
                                     https://github.com/NickAdfor/The-polynomial-method-and-restricted-sums-of-congruence-classes
  LeanPool/Polytopes                 https://github.com/Jun2M/Main-theorem-of-polytopes
  LeanPool/PumpingCfg                https://github.com/AlexLoitzl/pumping_cfg
  LeanPool/PythagoreanPolynomialParametrization
                                     https://github.com/epfl-lara/AutoformalizedProjects
  LeanPool/QuadraticIterates         https://github.com/MichaelStollBayreuth/QuadraticIterates
  LeanPool/Rado                      https://github.com/rkirov/jordan_pick
  LeanPool/RamanujanNagell           https://github.com/BarinderBanwait/ramanujan_nagell
  LeanPool/RellichKondrachov         https://github.com/abenenson/rellich-kondrachov
  LeanPool/RiemannMappingTheorem     https://github.com/vbeffara/RMT4
  LeanPool/RootSystem                https://github.com/Antoine-dSG/root_system
  LeanPool/RungeKuttaOrderConditions https://github.com/karlesmarin/runge-kutta-order-conditions-lean
  LeanPool/Rupert                    https://github.com/dwrensha/Rupert.lean
  LeanPool/Sabidussi                 https://github.com/gexahedron/sabidussi-lean
  LeanPool/SardMoreira               https://github.com/urkud/SardMoreira
  LeanPool/SelbergSieve4             https://github.com/amellendijk/selberg-sieve4
  LeanPool/SemicircleCheck           https://github.com/Wondermonger-daydreaming/semicircle-catalan
  LeanPool/Sensitivity               https://github.com/SamuelSchlesinger/sensitivity-conjecture
  LeanPool/SetTheory                 https://github.com/znssong/SetTheory
  LeanPool/SingularModuli            https://github.com/ElodinLaarz/lean-thesis
  LeanPool/SpectralPositivity        https://github.com/mrdouglasny/spectral-positivity
  LeanPool/SumsThreeSquares          https://github.com/pitmonticone/SumsThreeSquares
  LeanPool/Sundogcert                https://github.com/humiliati/sundogcert
  LeanPool/SyntheticEuclid4          https://github.com/ah1112/synthetic_euclid_4
  LeanPool/ThreeGap                  https://github.com/ElVec1o/five-distance-sharp
  LeanPool/Turan3                    https://github.com/ro-gut/turan3
  LeanPool/UlmsTheorem               https://github.com/elanroth/UlmsTheorem
  LeanPool/UnconditionalSchauderBasis
                                     https://github.com/SmaniaD/UnconditionalSchauderBasis
  LeanPool/VirasoroProject           https://github.com/kkytola/VirasoroProject
  LeanPool/Vlasov                    https://github.com/Hydrodynamical/Vlasov_Meanfield_Formalization
  LeanPool/WhiteheadTheorem          https://github.com/jzxia/WhiteheadTheorem
  LeanPool/ZFLean                    https://github.com/VTrelat/ZFLean
  LeanPool/Zeta3Irrational           https://github.com/ahhwuhu/zeta_3_irrational
  LeanPool/ZetaZeros                 https://github.com/AxiomMath/ZetaZeros
  LeanPool/ZhangYeungInequality      https://github.com/cboone/zhang-yeung-inequality


--------------------------------------------------------------------------------
Projects originally licensed under the MIT License
--------------------------------------------------------------------------------

These projects were imported from repositories licensed under the MIT License.
The MIT License grants the right to sublicense, so these projects are
redistributed here under the Apache License, Version 2.0. As the MIT License
requires, the original copyright notices are preserved below, together with the
MIT permission notice that follows them.

  LeanPool/AgreeToDisagree           https://github.com/AxiomMath/AgreeToDisagree
  LeanPool/ArtinWedderburn           https://github.com/JobPetrovcic/ArtinWedderburn
      Copyright (c) 2024 Job Petrovčič

  LeanPool/Biswal                    https://github.com/AxiomMath/Biswal
  LeanPool/Brouwer                   https://github.com/math-xmum/Brouwer
      Copyright (c) 2025 Math_XMUM

  LeanPool/CommonNeighbourConjecture https://github.com/alunik/common-neighbour-conjecture
  LeanPool/CutAndProject             https://github.com/dkunert/cut-and-project
      Copyright (c) 2026 Dirk Kunert

  LeanPool/DeadEnds                  https://github.com/AxiomMath/dead-ends
      Copyright (c) 2026 Axiom Math

  LeanPool/DirectedTopologyLean4     https://github.com/Dominique-Lawson/Directed-Topology-Lean-4
      Copyright 2023 Dominique Lawson

  LeanPool/FactorizationSystems      https://github.com/ivankobe/FactorizationSystems
      Copyright (c) 2024 ivankobe

  LeanPool/FelConjecture             https://github.com/AxiomMath/fel-polynomial
      Copyright (c) 2026 Axiom Math

  LeanPool/FormalizationOfBoundedArithmetic
                                     https://github.com/ruplet/formalization-of-bounded-arithmetic
      The upstream MIT LICENSE file leaves the copyright line as the unfilled
      template text "Copyright (c) [year] [fullname]"; the repository owner of
      record is "ruplet".

  LeanPool/HSDInteriorPointLP        https://github.com/makoto-yamashita/proof-on-a-homogeneous-self-dual-interior-point-method-for-linear-programming
  LeanPool/KaltonRoberts             https://github.com/boonsuan/KaltonRoberts
  LeanPool/Kuramoto                  https://github.com/velvetmonkey/kuramoto-lean
  LeanPool/LatticeTriangle           https://github.com/AxiomMath/lattice-triangle
      Copyright (c) 2026 Axiom Math

  LeanPool/Lean4Itree                https://github.com/mit-plv/lean4-itree
      Copyright (c) 2025 the choice-tree authors (see the AUTHORS file)

  LeanPool/LeanStationaryHarmonicMaps
                                     https://github.com/BrookWW/LeanStationaryHarmonicMaps
  LeanPool/PCFTheory                 https://github.com/YnirPaz/PCF-Theory
      The upstream MIT LICENSE file contains no copyright line; the repository
      owner of record is "YnirPaz".

  LeanPool/PLAcceleratedNesterovLean https://github.com/M1ngXU/PL-Accelerated-Nesterov-Lean
  LeanPool/PartialCombinatoryAlgebras
                                     https://github.com/andrejbauer/partial-combinatory-algebras
      Copyright (c) 2024 Andrej Bauer

  LeanPool/PartialRegularity         https://github.com/AxiomMath/partial-regularity
      Copyright (c) 2026 Axiom Math

  LeanPool/PolyaEnumerationTheorem   https://github.com/Luka-O/polya-enumeration-theorem
      Copyright (c) 2024 Luka-O

  LeanPool/QuasiBorelSpaces          https://github.com/YellPika/quasi-borel-spaces
      Copyright (c) 2025 Anthony Vandikas, Kiarash Sotoudeh

  LeanPool/RamanujanTauMissesPrimes  https://github.com/AxiomMath/ramanujan-tau-misses-primes
      Copyright (c) 2026 Axiom Math

  LeanPool/Redhill                   https://github.com/Parcly-Taxel/Redhill
      Copyright (c) 2026 Jeremy Tan / Parcly Taxel

  LeanPool/RlTheoryInLean            https://github.com/ShangtongZhang/rl-theory-in-lean
      Copyright (c) 2025 Shangtong Zhang

  LeanPool/SemicircleLaw             https://github.com/FredRaj3/SemicircleLaw
      Copyright (c) 2025 FredRaj3

  LeanPool/Shannon1948Formalization  https://github.com/SamuelSchlesinger/shannon-1948-formalization
      The upstream MIT LICENSE file gives the copyright line as
      "Copyright (c) 2026" with no name; the repository owner of record is
      "SamuelSchlesinger".

  LeanPool/SpecialNumbers            https://github.com/provables/special-numbers
      Copyright (c) 2024 Walter Moreira, Joe Stubbs

  LeanPool/SteinhausThreeGap         https://github.com/dkunert/three-gap-theorem-lean
      Copyright (c) 2026 Dirk Kunert

  LeanPool/TwoColoringOneRound       https://github.com/suomela/2-coloring-1-round
      Copyright (c) 2026 Jukka Suomela

  LeanPool/ZetaH123                  https://github.com/AxiomMath/zeta-h123

  MIT License -- the following permission notice applies to every project
  listed in this section:

  Permission is hereby granted, free of charge, to any person obtaining a copy
  of this software and associated documentation files (the "Software"), to deal
  in the Software without restriction, including without limitation the rights
  to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
  copies of the Software, and to permit persons to whom the Software is
  furnished to do so, subject to the following conditions:

  The above copyright notice and this permission notice shall be included in all
  copies or substantial portions of the Software.

  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
  IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
  FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
  AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
  LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
  OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
  SOFTWARE.


--------------------------------------------------------------------------------
Projects relicensed by their original author
--------------------------------------------------------------------------------

These projects were relicensed by their sole author before import.

  LeanPool/Clawristotle              https://github.com/Vilin97/Clawristotle
  LeanPool/ForwardEuler              https://github.com/Vilin97/forward_euler
      Originally distributed without a license file, then placed under the
      Apache License, Version 2.0, by its sole author.

  LeanPool/GrothendieckVanishing     https://github.com/Vilin97/Clawristotle
      Originally distributed under the Creative Commons
      Attribution-NonCommercial-ShareAlike 4.0 International license, then
      relicensed under the Apache License, Version 2.0, by its sole author.


--------------------------------------------------------------------------------
Additional upstream attribution and citation notices
--------------------------------------------------------------------------------

The following notices are reproduced from the upstream repositories' own NOTICE
files or LICENSE addenda. Only each project's Apache-2.0 Lean sources were
imported here; these notes preserve attribution and citation requests made by
the original authors.

  LeanPool/FormalLearningTheory      https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel
      The upstream LICENSE appends a citation request. The original author asks
      that publications, software, or derivative works built on this
      formalization cite:

          Gupta, D. (2026). Formal Learning Theory Kernel: Lean4 Formalization
          of the Fundamental Theorem of Statistical Learning.
          https://github.com/Zetetic-Dhruv/formal-learning-theory-kernel

  LeanPool/ZhangYeungInequality      https://github.com/cboone/zhang-yeung-inequality
      The upstream repository ships a NOTICE file (Apache License, Version 2.0,
      Section 4(d)). Its attribution notice reads:

          The Zhang-Yeung Inequality
          Copyright 2026 Christopher Boone

      The upstream additionally carries CC-BY-4.0 prose, CC-BY-SA-4.0 for its
      code of conduct, CC0-1.0 for generated files, and bundled reference
      materials under a custom license; none of those files were imported.