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 the project registry. 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 the project registry
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/ACMax                     https://github.com/MerLeanProver/ACMaxConjecture
  LeanPool/AFormalizationOfBorelDeterminacyInLean
                                     https://github.com/sven-manthe/A-formalization-of-Borel-determinacy-in-Lean
  LeanPool/AbstractLinearControl     https://github.com/frederic-marbach/alcs
  LeanPool/AharoniKorman             https://github.com/b-mehta/AharoniKorman
  LeanPool/AndersonConjecture        https://github.com/frenzymath/Anderson-Conjecture
  LeanPool/AnomalousDiffusion        https://github.com/scottnarmstrong/AVAnomalousDiffusion
  LeanPool/Apportionment             https://github.com/mdbrnowski/apportionmentlib
  LeanPool/ArchonFirstProofResults   https://github.com/frenzymath/Archon-FirstProof-Results
  LeanPool/ArnoldKAM                 https://github.com/ybq1415926-droid/arnold1963-kam
  LeanPool/AsymptoticTrianglePacking https://github.com/jtraverso/erdos-81-chordal-clique-partitions
  LeanPool/BKARForestFormula         https://github.com/scottnarmstrong/bkarforestformula
  LeanPool/BannaiBannaiStanton       https://github.com/AntoineduFresne/Bannai-Bannai-Stanton_Theorem
  LeanPool/BeckFialaMatrix           https://github.com/jtraverso/lean-pool
  LeanPool/Besicovitch               https://github.com/CoolRmal/Besicovitchs-1-2
  LeanPool/BeyondBethe               https://github.com/nimaanari/formalization-beyond-bethe
  LeanPool/BicausalOT                https://github.com/maxwellapexlab/bicausalot-palomar
  LeanPool/BlockSpectralSensitivity  https://github.com/Timeroot/BS_Lam
  LeanPool/BollobasNikiforov         https://github.com/ShengtongZhang-alt/BN
  LeanPool/BooleanIsoperimetry       https://github.com/AlexeyMilovanov/BooleanIsoperimetry
  LeanPool/BrauerGroupNew            https://github.com/Whysoserioushah/BrauerGroup
  LeanPool/BrillNoetherGraphs        https://github.com/npflueger/brill-noether-graphs
  LeanPool/BrooksSubcubic            https://github.com/jtraverso/lean-pool
  LeanPool/BruhatTits                https://github.com/chrisflav/bruhat-tits
  LeanPool/Burkholder                https://github.com/SmaniaD/Burkholder
  LeanPool/CIVAxisymmetric           https://github.com/scottnarmstrong/CIVAxisymmetric
  LeanPool/CaffarelliKohnNirenberg   https://github.com/scottnarmstrong/CaffarelliKohnNirenberg
  LeanPool/CarlsonFunctions          https://github.com/bjbraams/lean-codes
  LeanPool/CencovPetz                https://github.com/abenenson/cencov-petz
  LeanPool/CenteredMaximal           https://github.com/CoolRmal/centered-maximal-constant
  LeanPool/Champernowne              https://github.com/OldMathematician/ChampernowneNormality
  LeanPool/ChannelCapacity           https://github.com/abenenson/channel-capacity
  LeanPool/ChipFiring                https://github.com/dhyeymavani2003/chip-firing-with-lean
  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/CompactnessAndDegeneracy  https://github.com/openai/ten-proofs
  LeanPool/CompositionAlgebras       https://github.com/ehrlich-b/composition-algebras
  LeanPool/Computability             https://github.com/tannerduve/computability
  LeanPool/ComputableReal            https://github.com/Timeroot/computableReal
  LeanPool/ConcentrationInequalities https://github.com/jtraverso/erdos-81-chordal-clique-partitions
  LeanPool/ConnesKreimer             https://github.com/karlesmarin/connes-kreimer-lean
  LeanPool/ConnesRigidity            https://github.com/utensil/connes-rigidity
  LeanPool/ConwayRefinement          https://github.com/gaearon/conway-refinement
  LeanPool/CramerWold                https://github.com/Lemmy00/lean-pool
  LeanPool/CriticalPortraits         https://github.com/no-way-labs/lean-critical-portraits
  LeanPool/DavisKahan                https://github.com/aiq-kitware/aiq-davis-kahan-1970-rotation-eigenvectgors-perturbation-formalization
  LeanPool/DemazureOperatorsLean     https://github.com/bolito2/DemazureOperatorsLean
  LeanPool/DemazureProduct           https://github.com/npflueger/demazure
  LeanPool/DensityHalesJewett        https://github.com/gdahia/densityhalesjewett
  LeanPool/Desargues                 https://github.com/oneofvalts/desargues
  LeanPool/Dilatations               https://github.com/rndmx/DilCat
  LeanPool/DistanceGeometry          https://github.com/lyfar/distance-geometry-lean
  LeanPool/DomainTheory              https://github.com/catskillsresearch/domain_theory
  LeanPool/DrossFractionalTriangleDecomposition
                                     https://github.com/jtraverso/erdos-81-chordal-clique-partitions
  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/EhrhartVolumeInequality   https://github.com/openai/ten-proofs
  LeanPool/EilenbergZilber           https://github.com/jeffrey-dot-li/lean-homology
  LeanPool/EllipticPDE               https://github.com/alejandro-soto-franco/EllipticPDE
  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/Erdos548                  https://github.com/tadamcz/erdos548
  LeanPool/Erdos81PaperIContrib      https://github.com/jtraverso/erdos-81-chordal-clique-partitions
  LeanPool/Erdos81PaperIIContrib     https://github.com/jtraverso/lean-pool
  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/EscauriazaSereginSverak   https://github.com/scottnarmstrong/EscauriazaSereginSverak
  LeanPool/EuclideanJordan           https://github.com/ehrlich-b/euclidean-jordan
  LeanPool/EvenGraphCycles           https://github.com/jtraverso/erdos-81-chordal-clique-partitions
  LeanPool/EventStructures           https://github.com/vikraman/event-structures
  LeanPool/ExpChaotic                https://github.com/LR-UK/exp-chaotic
  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/FormalizingGMT            https://github.com/uw-math-ai/FormalizingGMT
  LeanPool/FriezePatterns            https://github.com/Antoine-dSG/frieze_patterns
  LeanPool/FrontierMathOpenHypergraphs
                                     https://github.com/math-inc/FrontierMathOpen-Hypergraphs
  LeanPool/FullyDynamicMatching      https://github.com/ykanoria/fd1d-lean
  LeanPool/FundamentalInequality     https://github.com/linzialessandro/FundamentalInequality
  LeanPool/GKPCarry                  https://github.com/lyfar/gkp-carry-lean
  LeanPool/GapCVP                    https://github.com/openai/ten-proofs
  LeanPool/GoemansFlow               https://github.com/jyh/dinitz-verify
  LeanPool/GranvilleMoore            https://github.com/AxiomMath/GranvilleMoore
  LeanPool/GraphColouringMatching    https://github.com/jtraverso/lean-pool
  LeanPool/GrothendieckBessel        https://github.com/lukasliehr/GrothendieckBessel
  LeanPool/HadwigerNelsonBounds      https://github.com/lyfar/hadwiger-nelson-bounds-lean
  LeanPool/HansonWright              https://github.com/Lean-MoDS/StatsMLlib
  LeanPool/HardSphereNBC             https://github.com/ukiyois/hs-virial-nbc-identity
  LeanPool/HasseMinkowski            https://github.com/jayyswan/hasse-minkowski
  LeanPool/HighContrastHomogenization
                                     https://github.com/scottnarmstrong/HighContrastHomogenization
  LeanPool/HopfProblem               https://github.com/plby/HopfProblem
  LeanPool/Incompleteness            https://github.com/FormalizedFormalLogic/Incompleteness
  LeanPool/InfinitaryLogic           https://github.com/cameronfreer/infinitary-logic
  LeanPool/InfiniteConnesRigidity    https://github.com/openai/ten-proofs
  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/Koethe                    https://github.com/tadamcz/koethe
  LeanPool/Komlos                    https://github.com/gdahia/Komlos
  LeanPool/KrafftSieve               https://github.com/ElNando888/KrafftSieve
  LeanPool/KrohnRhodes               https://github.com/adii800/krohn-rhodes-lean
  LeanPool/Kurosh                    https://github.com/Arthur742Ramos/KuroshSubgroupTheorem
  LeanPool/LanguageGeneration        https://github.com/xiaoyulics/language-generation-characterization
  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/LiCriterion               https://github.com/nicholasbulka/li-criterion-rh-equivalence-lean
  LeanPool/LiebThirring              https://github.com/scottnarmstrong/LiebThirring
  LeanPool/ListEdgeColoringComplete  https://github.com/jtraverso/haggkvist-janssen
  LeanPool/LocalComplexGeometry      https://github.com/BochaoKong/nullstellensatz
  LeanPool/LongGapsBetweenPrimes     https://github.com/openai/LongGapsBetweenPrimes
  LeanPool/LowDimSolvClassification  https://github.com/LieLean/LowDimSolvClassification
  LeanPool/LowWeightPauliDynamics    https://github.com/Jue-Xu/Lean4LPD
  LeanPool/MRiscX                    https://github.com/JulsDE/MRiscX
  LeanPool/Malliavin                 https://github.com/savarin/lean-malliavin
  LeanPool/MarkoffModP               https://github.com/yuma-mizuno/markoff-modp
  LeanPool/MarkovProcess             https://github.com/scottnarmstrong/markovprocess
  LeanPool/MarshallHall              https://github.com/arthur742ramos/marshallhalltheorem
  LeanPool/MassFormula               https://github.com/0stellensatz/MassFormula
  LeanPool/MatchingLogic             https://github.com/eveil-labs/matching-logic-lean
  LeanPool/MaxFlowMinCut             https://github.com/jtraverso/erdos-81-chordal-clique-partitions
  LeanPool/MetricCodes               https://github.com/openai/ten-proofs
  LeanPool/MicrowaveNetworks         https://github.com/matteonerini/formalizing-analog-computing
  LeanPool/MinModulusUniqueMultisetSum
                                     https://github.com/jarfo/min-modulus
  LeanPool/MinimumDegreeMatching     https://github.com/jtraverso/erdos-81-chordal-clique-partitions
  LeanPool/MisereGames               https://github.com/t4ccer/misere-games
  LeanPool/Monlib4                   https://github.com/themathqueen/monlib4
  LeanPool/Monsky                    https://github.com/dhyan-aranha/Monsky
  LeanPool/MooreBound                https://github.com/woutercvb/wewantmoore
  LeanPool/MoserLatticeColorings     https://github.com/lyfar/moser-lattice-colorings-lean
  LeanPool/MovingSofa                https://github.com/deancureton/MovingSofa
  LeanPool/MulticolorTriangleRamsey  https://github.com/openai/ten-proofs
  LeanPool/NFWeakPartition           https://github.com/elliotglazer/nf-not-wpp
  LeanPool/NagataFactoriality        https://github.com/arthur742ramos/nagatafactoriality
  LeanPool/NandakumarRamanaRao       https://github.com/akopjan/nrr-aak
  LeanPool/NashEmbedding             https://github.com/langlerangle/nashembedding
  LeanPool/NashWilliams              https://github.com/yannpequignot/TwoBQO
  LeanPool/NavierStokesAndEuler      https://github.com/openai/NavierStokesAndEuler
  LeanPool/NemytskiiLebesgue         https://github.com/madvorak/nemytskii-lebesgue
  LeanPool/Neukirch                  https://github.com/jjdishere/neukirch
  LeanPool/Nikodym                   https://github.com/shengtongzhang-alt/nikodym
  LeanPool/NonSoficGroup             https://github.com/openai/ten-proofs
  LeanPool/OSforGFF                  https://github.com/mrdouglasny/OSforGFF
  LeanPool/OddPrimeValuationDistribution
                                     https://github.com/lyfar/gkp-carry-lean
  LeanPool/Odlyzko                   https://github.com/ImperialCollegeLondon/FLT
  LeanPool/OneManifold               https://github.com/sweeneyde/1mfld
  LeanPool/OperatorTheory            https://github.com/savarin/lean-operator-theory
  LeanPool/OrderClosures             https://github.com/pedrotradacete/OrderClosures
  LeanPool/OrderPQ                   https://github.com/wupr/order-p-q
  LeanPool/PDL                       https://github.com/m4lvin/lean4-pdl
  LeanPool/PFR                       https://github.com/teorth/pfr
  LeanPool/PaperIVCliqueTree         https://github.com/jtraverso/erdos-81-chordal-clique-partitions
  LeanPool/ParallelPostulate         https://github.com/Richiesutie/ParallelPostulate
  LeanPool/ParameterFreeGradient     https://github.com/yuningyang19/parameter_free_gradient_p
  LeanPool/PebblingLean              https://github.com/pachterlab/P_2026_2
  LeanPool/PentagonalNumberTheorem   https://github.com/wwylele/PentagonalNumberTheorem
  LeanPool/PentagonalNumberTheoremAnalytic
                                     https://github.com/viazovska/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/PolylogIntegrals          https://github.com/rainrzk/LeanPolyLog
  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/Puiseux                   https://github.com/deancureton/Puiseux
  LeanPool/PumpingCfg                https://github.com/AlexLoitzl/pumping_cfg
  LeanPool/PureNock                  https://github.com/nockchain/pure-nock-lean
  LeanPool/PythagoreanPolynomialParametrization
                                     https://github.com/epfl-lara/AutoformalizedProjects
  LeanPool/QECCertificates           https://github.com/QCL-SUAT/QECCertificates
  LeanPool/QuadraticCarleson         https://github.com/anastasiosfragkosmath/quadratic-carleson-palomar-submission
  LeanPool/QuadraticIterates         https://github.com/MichaelStollBayreuth/QuadraticIterates
  LeanPool/QuantumParallelRepetition https://github.com/openai/ten-proofs
  LeanPool/QuantumQuery              https://github.com/troyjlee/quantum-query-complexity
  LeanPool/Rado                      https://github.com/rkirov/jordan_pick
  LeanPool/RamanujanNagell           https://github.com/BarinderBanwait/ramanujan_nagell
  LeanPool/RearrangementNumber       https://github.com/vo-rodrigues/rr-equals-nonmeager-paper
  LeanPool/RegtsSevenster            https://github.com/willwhistler/regts-sevenster
  LeanPool/RellichKondrachov         https://github.com/abenenson/rellich-kondrachov
  LeanPool/RiemannMappingTheorem     https://github.com/vbeffara/RMT4
  LeanPool/RiemannRochFunctionFields https://github.com/vaca22/riemann-roch-function-fields
  LeanPool/RootSystem                https://github.com/Antoine-dSG/root_system
  LeanPool/RungeKuttaOrderConditions https://github.com/karlesmarin/runge-kutta-order-conditions-lean
  LeanPool/RunsOfMultiples           https://github.com/jas-ho/runs-of-multiples-lean
  LeanPool/Rupert                    https://github.com/dwrensha/Rupert.lean
  LeanPool/SNumbers                  https://github.com/mario-ullrich/lean-snumbers
  LeanPool/Sabidussi                 https://github.com/gexahedron/sabidussi-lean
  LeanPool/SardMoreira               https://github.com/urkud/SardMoreira
  LeanPool/Schoenflies               https://github.com/alonamaloh/schoenflies-lean
  LeanPool/ScottMeasurement          https://github.com/catskillsresearch/scott1964
  LeanPool/SelbergSieve4             https://github.com/amellendijk/selberg-sieve4
  LeanPool/SemicircleCheck           https://github.com/Wondermonger-daydreaming/semicircle-catalan
  LeanPool/Sendov                    https://github.com/teorth/sendov
  LeanPool/Sensitivity               https://github.com/SamuelSchlesinger/sensitivity-conjecture
  LeanPool/SetTheory                 https://github.com/znssong/SetTheory
  LeanPool/SeveralComplexVariables   https://github.com/bjbraams/lean-scv
  LeanPool/SingularModuli            https://github.com/ElodinLaarz/lean-thesis
  LeanPool/SpectralPositivity        https://github.com/mrdouglasny/spectral-positivity
  LeanPool/SpectralTheory            https://github.com/savarin/lean-spectral-theory
  LeanPool/SpherePacking             https://github.com/openai/ten-proofs
  LeanPool/Stafford38                https://github.com/itpplasma/stafford38-formal
  LeanPool/StallingsFolding          https://github.com/Arthur742Ramos/stallings-folding
  LeanPool/StructuralGraphClasses    https://github.com/jtraverso/lean-pool
  LeanPool/SumDifferenceExponent     https://github.com/linhaowei1/sum-diff-proof
  LeanPool/SumsThreeSquares          https://github.com/pitmonticone/SumsThreeSquares
  LeanPool/Sundogcert                https://github.com/humiliati/sundogcert
  LeanPool/Superorthogonality        https://github.com/roos-j/lean-superorthogonality
  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/TuttePath                 https://github.com/mbaker386/tutte-homotopy-lean
  LeanPool/UlmsTheorem               https://github.com/elanroth/UlmsTheorem
  LeanPool/UnconditionalSchauderBasis
                                     https://github.com/SmaniaD/UnconditionalSchauderBasis
  LeanPool/VirasoroProject           https://github.com/kkytola/VirasoroProject
  LeanPool/ViscositySolutionTheory   https://github.com/willmfeldman/viscosity-solution-theory
  LeanPool/Vizing                    https://github.com/jtraverso/erdos-81-chordal-clique-partitions
  LeanPool/Vlasov                    https://github.com/Hydrodynamical/Vlasov_Meanfield_Formalization
  LeanPool/Wallace                   https://github.com/vo-rodrigues/wallace-problem-zfc-paper
  LeanPool/WhiteheadTheorem          https://github.com/jzxia/WhiteheadTheorem
  LeanPool/ZFLean                    https://github.com/VTrelat/ZFLean
  LeanPool/Zeta32                    https://github.com/dtq1997/zeta2-zeta3-linear-independence
  LeanPool/Zeta3Irrational           https://github.com/ahhwuhu/zeta_3_irrational
  LeanPool/Zeta5Irrational           https://github.com/mo271/Zeta5
  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/BooleanMultiplication     https://github.com/GregoryMorse/unrestricted-boolean-mul
  LeanPool/Brouwer                   https://github.com/math-xmum/Brouwer
      Copyright (c) 2025 Math_XMUM

  LeanPool/Chvatal                   https://github.com/boonsuan/chvatal
  LeanPool/CommonNeighbourConjecture https://github.com/alunik/common-neighbour-conjecture
  LeanPool/ConwaySoifer              https://github.com/AnanasClassic/conway-soifer-n3-lean
  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/ErdosGinzburgZiv          https://github.com/zakharov2k/egz-formal-proof
  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/FourAP                    https://github.com/boonsuan/4ap
  LeanPool/GaussianMomentsCounterexamples
                                     https://github.com/long-mathematics/gaussian-moments-counterexamples
  LeanPool/HSDInteriorPointLP        https://github.com/makoto-yamashita/proof-on-a-homogeneous-self-dual-interior-point-method-for-linear-programming
  LeanPool/InflationTermination      https://github.com/williamjblair/inflation-termination
  LeanPool/KaltonPeck                https://github.com/adas1236/KaltonPeck
  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/NaslundCounterexample     https://github.com/JD-Jones-ASES/ns-lean
  LeanPool/Nivat                     https://github.com/boonsuan/nivat
  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/PersistentSOS             https://github.com/JD-Jones-ASES/persistent-sos
  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/SalemTheorem              https://github.com/stalex444/salem-theorem
  LeanPool/ScottishBook155           https://github.com/yoshito-ishiki-math/lean-scottish-book-155
  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/SmallUndecidableGroups    https://github.com/32805433/Adian-Rabin
  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/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/Erdos548                  https://github.com/tadamcz/erdos548
      The upstream repository ships a NOTICE file (Apache License, Version 2.0,
      Section 4(d)). Its attribution notice reads:

          Erdős problem #548 (Erdős–Sós conjecture): proof
          Copyright 2026 Tom Adamczewski / Epoch AI

          The formal statement was given to the AI system by the FrontierMath
          Erdős benchmark of Tom Adamczewski and Thomas F. Bloom
          (LeanOpenProblems, https://github.com/epoch-research/LeanOpenProblems,
          commit 77882c437ca1dfefab3b27fa00f1d29788100311), Epoch AI, MIT License.
          The Lean proofs were produced by a pre-release version of GPT-6 Astra
          (OpenAI) running in that benchmark.

  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/HasseMinkowski            https://github.com/jayyswan/hasse-minkowski
      The source repository at commit
      47f0e9b5cba6e6354b882bc5856a11962ba61f4a ships the following NOTICE.
      Its HasseMinkowski/ paths are vendored under LeanPool/HasseMinkowski/.

      The Hasse–Minkowski theorem, formalized in Lean 4
      Copyright (c) 2026 jayyswan

      This product includes software developed as part of this project.
      Licensed under the Apache License, Version 2.0 (see the file LICENSE).

      ================================================================================
      Third-party material
      ================================================================================

      Portions of `HasseMinkowski/` are derived from the "HassePrinciple" project:

          https://github.com/mariainesdff/HassePrinciple
          Copyright (c) 2026 Nirvana Coppola, Maria Ines de Frutos-Fernandez.
          All rights reserved.
          Licensed under the Apache License, Version 2.0.

      HassePrinciple is a collaborative formalization from the Women in Numbers 7
      workshop, led by Nirvana Coppola and Maria Ines de Frutos-Fernandez, with
      project members Mallory Dolorfino, Kate Finnerty, Cathy Hsu and Chi-Yun Hsu.

      The following files of this project are derived works.  Each one carries the
      upstream authors in its own file header, and each has been modified: the
      statements and proofs were rewritten against Lean 4.33 / Mathlib without the
      upstream module system, and the material was extended beyond what upstream
      proves.

          HasseMinkowski/HilbertSymbol/Existence.lean
              derived from HassePrinciple/HilbertSymbol/ExistenceTheorem.lean
              (the S / T / A / M construction and the lemmas named after it)

          HasseMinkowski/Padics/Squares.lean
              derived from HassePrinciple/Padics/Squares.lean and
              HassePrinciple/Padics/Lemmas.lean
              (PadicInt.isSquare_of_zmod, PadicInt.isSquare_of_zmodPow, and the
              open-subgroup argument for p-adic unit squares)

          HasseMinkowski/RankCriteria.lean
              derived from HassePrinciple/QuadraticForm/HasseMinkowskiInvariant.lean
              (the rank-two and rank-three local representability criteria)

      The remaining files of `HasseMinkowski/` are original to this project.  In
      particular, the results that upstream leaves as `sorry` -- the rank-three
      local-global step, the rank-four case, the rank >= 5 induction (Meyer), the
      2-adic Hilbert symbol formula, Hilbert reciprocity, and the assembled
      `hasseMinkowski` and `meyer` theorems -- are proved here independently.

      Upstream naming conventions are followed throughout so that the two
      developments can be compared declaration by declaration.

  LeanPool/Koethe                    https://github.com/tadamcz/koethe
      The upstream repository ships a NOTICE file (Apache License, Version 2.0,
      Section 4(d)). Its attribution notice reads:

          Köthe conjecture: disproof (Krempa's matrix form)
          Copyright 2026 Tom Adamczewski / Epoch AI

          This repository includes a definition and a conjecture statement copied
          from Formal Conjectures (https://github.com/google-deepmind/formal-conjectures,
          file FormalConjectures/Wikipedia/Koethe.lean at commit
          9cbe1d3c12998c786b7c2cd99ce28a21b6631f66), Copyright 2025 The Formal
          Conjectures Authors, licensed under the Apache License, Version 2.0.

          The formal statement was given to the AI system by Epoch AI's
          LeanOpenProblems harness (https://github.com/epoch-research/LeanOpenProblems,
          branch wikipedia-dataset, commit 0ef96d7b12cfa96a93761b4bba1c635f4546c5ca),
          MIT License. The Lean proof was produced by a pre-release version of
          GPT-6 Astra (OpenAI) running in that harness.

  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.