Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

A counterexample to Hadwiger's conjecture

lax-342547·formalized by Édouard Bonnet @EdouardBonnet · OpenAI · Codex 6.1·created ·GitHub @1e7d18c·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    Abstract

    We formalize OpenAI's construction of graphs of arbitrarily large order mm with independence number at most two and pairwise touching-matching number less than m/100m/100.

    We reuse OpenAI's partial Lean formalization released with the original paper: Proposition 3.5, the matching-minor bound and its ordinary chromatic consequence. We also adapt OpenAI's later complete binary-frame construction from a separately pinned upstream revision. This submission ports that development to the archive's Lean and mathlib versions, connects it to the archive's definitions by definitional equality, and organizes the definitions, statements, and proofs for Lax. The original and later upstream revisions, adaptations, and source hashes are recorded in the repository's provenance files.

    The proved matching-minor inequality 3h(G)≤m+4cm⁡(G)+23h(G)\le m+4\operatorname{cm}(G)+2, together with ordinary and fractional coloring bounds, yields h(G)<26m/75+2/3<m/2≤χf(G)≤χ(G)h(G)<26m/75+2/3<m/2\le\chi_f(G)\le\chi(G) for m≥5m\ge5. Both counterexample consequences use the actual construction proof.

    Concepts

    Concept map
    372 concepts
    100%
    Finite accepting-family lossesActual finite accepting-pair injectionActual gradient-realized cells in the collisionaveraging lawActual projected span deficitChannel bounds with adaptive protectedcoefficient spacesSampling after exposed coordinatesAdaptive sampling on disjoint coordinatesetsUnion over adaptive component coversExact-image bounds for independent affinecolumnsIndependent nominal affine slices from thefree blockUniform quantitative thresholds foraffine-slice varianceConditioned affine-slice variance under theactual raw lawFinite amplified-test averagingIndependent free-direction spaces at distinctselector labelsActual point atoms determine cut-spacefunctionalsActual finite atom parameterization anddegreesOrdered atom products in the actualgradient formPoint atoms and finite flavor distributionsSparse unselected primal vectors in barredspaces lie in the pinsBarred response spaces and the actualobstruction rank budgetCompression preserving allowed pointmoments and the actual cut domainThe exact space of binary base momentsRank control for the frozen baseline onprimal inputsExact uniform bilinear character meanWalsh operator bounds with explicit bilinearrankBilinear parts of ordered evaluations onevery atom flavorSimultaneous binary mixer estimates for alllabels and flavorsFormal ordered product bits realizesymmetric correctionsBipartite capacity networksRank of a lifted tensor sumBoolean polynomial nonvanishing andexactificationBounded allowed derivatives preserving theactual linearized responsePeeling with bounded new rank andnormalized leaf lawsActual-mass averaging over retainedrecord-cell pairsPositive representatives of original retainedcellsSimultaneous assembly of opposite endpointsand reciprocal unit rolesAllowed channel changes and the actual tableinjection testsIndependent binary channel charactersActual raw frame channel phase tailsJoint channel law and itsindependent-column densityRank-controlled factorization throughallowed orthogonal channelsActual endpoint character productsActual channel moments and phase tailsThe chromatic lower bound for independencenumber twoClique minors and the Hadwiger numberCoefficient phases as dot products ofrank-factor imagesQuantitative collision and squared restrictionexponentsExplicit pruning and scalar agreementexponent marginsPruning small unary record cellsUniform collision scales and boundednumerical optionsCombined column and row mode exposureCommon star atoms eliminate the diagonalpredictor coefficientExact common predictions on retained massMarginal transfer of common affine-slice testsJoint retained-cell characters across allcomponentsRows of diagonal tensor mapsMoment estimates for actual componenttensor phasesComponentwise no-cover rank growthComponentwise mode spaces and diagonaltensorsSimultaneous scalar Gram agreement acrosscomponentsA bounded-rank pure correction for theactual scalar recipeConcrete cut-space testers and the orderedmixer formConcrete coordinates, quadratic testers, andthe self-Gram formThe concrete finite frame model and itssampled graphsNumerical recipes prescribe the concretegradients on witness atomsConditional independence of the two channelframesThe affine minus-column law at a fixed plusframeConditional pair laws on original cellsActual conditioned affine coefficientdependence boundsExact finite conditioning of separated FouriertestsExact conditioning costs and recovery offinite probability massesConnected matchingsCompression that fixes pin/key vectors andpreserves target matricesSubexponential container counts at thepaper sample scaleEntropy progress for residual pair lawsFinite deterministic container recursionDimensions of the concrete coefficient spaceIndependence of distinct sample positionsThe row-corank bound for a uniform binarymatrixA counterexample to Hadwiger's conjectureRank preservation under mode-coveravoidanceJoin-stable classes of mode coversCount tensors killed by exposureActual exposure cover projectionActual tensor cover decomposition anddimensionQuantitative comparison after cross-batchGram conditioningIndependent characters of actual mutualGram entriesWell-defined cut functionalsCut profiles and the constant kernelMajority normalization of sparse cut profilesRank-one derivative tests are scalar pairingsof residual contractionsThe full linearized response on pairs ofactual cut profilesRank of a diagonal familyDisjoint pair exception tailsMoments across endpoint channel groupsOriginal-rank no-cover tails for endpointgroupsDyadic span deficit estimatesFixed dyadic moment orders at the ambientscaleA small dyadic tail scaleActual dyadic deficit recurrenceDimension and component-rank bounds foreffective test spacesFull response obstructions are effectiveprofiles plus selected atomsFinite empirical variance from atwo-coefficient comparisonExactification of actual vanishing pointpredictionsEntropy bounded container familiesEntropy along feasible mixture lines,including new supportFull feasible support and finite informationprojectionDeterministic entropy and neighborhoodselectionsExact image pins in nominal coefficientspacesProjection removes the exposed termsCount tested index occurrencesFinite ordered fingerprint budgetsThe paper fingerprint and exception scalesFinite accepted overlap to original hole massFinite pin-injection exceptionFinite linear images and their uniform-lawdensity boundsFinite even moment expansionFinite independent sampling and vertexexception tailsFixed-parameter endpoint-group phaseboundsUniform no-cover phase cancellation withfixed parametersUniform positive Gram mass from boundedtester prescriptionsStabilized ranks and the radical quotientAffine-slice comparison for every actual atomflavorReal max-flow min-cut from residualreachabilityPolar rank of the formal mixer quadraticActual gradient agreement and matched keysproduce all four cross holesTiny-cover four-bit parity boundsFinite scalar agreement from binarycharacter boundsOrdinary fractional coloringThe fractional-coloring counterexampleNonempty raw frame spacesAmbient symmetries and frame marginalsReciprocal raw-frame orientation and dualpin avoidanceUniform tuple images on prescribed GramorbitsFresh key directions are independent modulotable spacesThe simultaneous gradient corrections retainevery frozen pin and key entryBaseline bilinear extensions retaining allfrozen rows and columnsOriginal record cells determine the commonfrozen gradient targetExact agreement of zero quotient charactersWhole-space gradient realization preservingthe actual frozen entriesUnary records determine every frozen crossentryBaseline contractions on the selected atomsA good sample from the explicit containerbudgetAll four whole-space gradient equations fromassembled channel changesThe symmetric binary gradient formDeterministic whole-space gradientrealization from the genuine recipehypothesesGram-conditioned columns and theirrank-failure probabilityTwo-sided Gram normalization forindividually injective framesActual reference-batch laws for mutual GramtestsScalar agreement after quotient characterestimatesSampled graph failure boundGreedy independence of subspacesGreedy mode space exposureSmall actual greedy exposure tailsPhase density budgets for selected channelgroupsTwo-batch comparison across independentcomponent groupsEntrywise product rank and incompatibletuplesUniform relative Gram normalization errorsThe binary hole relationHoles are symmetric, loopless, andtriangle-freePaying the reference-image conditioning anddimension costsIndependent leaf mixtures preserve actualpair-event massesGreedy independent failure samplesAmplified channel failures on independentpinned spacesNo-cover rank growth on arbitrary finiteindicesRelative injection loss for polynomialaccepting massEarly channel choice and injection exponentbudgetsInjection parameter quantifiersAccepting-pair test unions and relative lossUniform injective-matrix densityUniform injective frames and channeltranspose failureExact joining of two prescribed Gram orbitsFrozen pin and key records with nominalcolumn budgetsAppend fresh directions to the independentkey tupleJoint-injectivity loss for two actual referencebatchesExact leaf entropy bounds joint key andadditional imagesJoint binary projections for commutingidempotentsBounded descriptions of large matrix kernelsAccepted key subprobabilities and uniformoverlapFresh point-ray spans are disjoint from thenominal table spacesLow-rank Boolean moments have boundedlabel supportTriangle relations separate into individuallabel blocksJoint matrix-image caps for retained leaflawsJoint fresh-image entropy on originalretained leaf cellsActual independent leaf averaging andoriginal-law collision costExtracting a leaf with all remainingexact-image capsAll-rank tuple image caps from exact-pin leafentropyFinite peeling into disjoint exact-pin leavesQuantitative trimming after restrictions of aleaf mixtureIdentification of the lifted tensor sumActual deficits indexed by a distinct listFinite list tail statisticsFactorization and counting of low-rankbinary matricesDimension deficits after an arbitrary modemapNo-cover phases with whole-unit marksCount matching occurrences covered byterminal exceptionsClique minors from connected matchingsMatching occurrences and raw unit typesFinite metadata and exact-image records foradditional pinsCompatibility and codimension offorward/reverse matrix restrictionsThe distribution of mixer rows on freedirectionsActual-mass recovery and residual boundsthrough finite splitsExposed mode dimension budgetExplicit no-cover moment parameter marginsIntersections of restricted moment spacesRecovery of low-rank Boolean moments fromlow degreesBoolean point moments with restricted basecoordinatesFinite moment probability and rank splitRaw phase estimates for dependent markedunitsA low rank sum supplies an actual adaptivecoverNo-cover phase momentsActual no-cover phase cancellation undermarginal densityRank growth without an adaptive modecoverThe 3K+28 baseline bound in the actualnominal coordinatesPrimal blocks of the nominal spaces andtheir bounded table partPure corrections realized by actual nonlinearchannel productsExact reference Gram-orbit marginals underinjective affine restrictionsIndependent ordered mixer blocks at distinctlabelsWeighted compatibility from inevitablesample pairsSquared restriction cost for independent uniteventsEndpoint projections of paired pure-responseannihilatorsPaired-frame orbit under the primal anddual actionsActual paired-witness key spaces satisfy thebaseline hypothesesBinary prescriptions at all endpoints of apaired scalar recipeFull paired witness lists and scalar recipeequationsTiny-cover pairing matrix rankPaper parameter graph probabilitySupersaturation to sampled graphs at thepaper parametersHigh probability sampled graph constructionIndependent parameter averaging withopposite-dependent original cellsFinite exposure partitionsRank and density budgets for exact-imagepeelingActual phase averages from small exceptionaltailsThe numerical no-cover phase marginSparse pin exclusions with arbitrary basecoefficientsExact-pin leaf entropy is invariant undernominal axis reindexingCommon predictions from actual pointtensorsBoolean degree of actual point-tensorevaluationsPolynomial degree of actual tensorevaluationsPrepared-unit injection on actual acceptingpairsEarly channel choice for preparedaccepting-pair injectionUniform primal-span avoidanceSparse residual contractions belong to theactual primal pinsActual primal-channel scalar tests andretained-cell four-hole probabilityFinite primal-channel records with the paperbit count and four-hole implicationRetractions with bounded rank on theprimal inputsExponential sampling failure marginExact images mixing independent injectiveframesJoint minus images after exposing severalplus framesCounting tuples of symmetric matrices withbounded total rankSplit quotient projections preserve coefficientcharactersProjected nonzero terms in the actualremaining sumOffsets constructed from the actual commonprojectionPrimal projections and preservation ofeffective spacesDimensions of projected mode spacesExact probabilities for independent protectedchannel imagesPure obstructions on the actual pair of cutprofilesExact pure-flavor tester room and alaw-uniform Gram mass floorWalsh bounds for independent image lawsand separated phasesQuadratic character bias on affine subspacesLinear point-tensor evaluations are BooleanquadraticsActual query keys independent modulo oldpinsActual query frozen spaces and linear recordexponentsReference keys and matched keys for actualpaired listsThe actual paired-list key slot budgetCompression on the actual barred nominalquotientsExtracting fresh label coefficients throughpin quotientsActual factor lifts and covered offsetsRank factors independent modulo the actualfrozen spacesRank of a tensor killed in two quotientspacesFull rank coefficient factorizationsRank loss under two restrictionsRank-controlled pure forms on the actualbarred quotientsRaw accepting-family injection withexponential lossBounded baselines for both actual crossorientationsBounded tests under the actual two-batchGram lawBoth actual cross orientations haveretained-cell image entropyActual frame observations realize thenominal channel contractionsActual raw frame observations with uniformtwo-batch decayRaw matrix frames and their tensorrealizationActual grouped raw observations witharbitrary common testsExponential bound for the raw intersectionexceptionActual joint key and fresh image capsThe finite uniform raw-vertex lawExact-pin peeling for the actual raw framelawActual raw primal-span avoidanceActual query-key image caps on raw leavesFour actual holes inside an original retainedcell pairSecond exact-pin peeling for the actual rawframe lawFinite supersaturation implies an actualsampled graphOriginal retained-cell laws from finite PMFsCompact real-capacity flows and amaximizing flowNonlinear channel realization of the actualwhole-space recipe residualGradient residuals vanish on effective profilesand selected atomsCoupled scalar recipes give consistent atomgradientsKey-indexed original record cellsJoint reference image caps across both signsand all drawsConstrained key reference spaces havepositive densityThe full reference cap for exact pin eventsFinite relative entropy and support costsResidual walk augmentation for real-capacityflowsRemoving selected atoms leaves onlyunselected component labelsThe bounded pure remainder of an actualscalar recipeMatrix representations and the boundedresidual rank ingredientsUnrestricted linearized solutions for actualscalar recipesTrimming a restricted family of exact-pinleavesRank loss under restriction of a bilinear formActual cross Gram characters on frozenunary cellsActual vanishing predictions on a retainedpopulationImage caps inside original retained cellsRight endpoint query-key caps via paired-listreindexingEventual sampling margins for the paperparametersGraphs sampled from a hole relationSimultaneous agreement of linear cross Gramtests on retained cellsFresh peeling after restrictions and deliberateextra pinsSelected tensor blocks of actual pureobstructionsA selected affine ray determines its momentblockSubtracting selected atoms preserves pureannihilationSelected label coefficients agree across thecut profileInterpolation of finitely many binary selectorlabelsFinite sequential testsAn actual common point with diagonaltester oneRandom sharp-block forms and theiralternating parityBit rank and Walsh bounds for globalvector-slot pairingsOne exposure controls both modesSmall phases on selected endpoint channelgroupsThe finite no-cover phase toleranceSmall affine slices force globalcross-coefficient rankCounting all bounded-dimensional protectedspacesNumerical cross tables, injection flags, andunary admissibilityMonotonicity of span deficitsMode space span deficitsSparse profiles from raw intersections(Lemma 4.4)Unselected sparse vectors cannot concealfresh key coefficientsA uniform label budget for all sparse pinvectorsSparse normalized representatives of sharedconcrete tensorsMass and density costs of splitting bymetadata and imagesLow-rank tester routing along tag starsNonzero tensor count from span deficitsRank of an actual linear map sumSymmetric low-rank factorization, includingcharacteristic twoConsistent symmetric binary prescriptions ontwo witness listsPositive pure-flavor mass for the actualsynthetic parity slice GramsQuantitative common-test error obstructionfor synthetic parityTable contractions on effective profiles andtheir full extensionsBounded table data and linear-size nominalcoefficient recordsActual table injection and ambient pinfailuresTable coordinates and private channelcomplementsMajority intersections in the cyclic taggeometryExplicit low-rank matrices for thewhole-space gradient targetThe fifteen-rank witness tester targetPure bilinear responses detect quotienttensorsQuotient extractors isolate individual tensorlabel blocksCharacters of all independent tensor channelsWell-defined channel contractions onprojected tensor spacesRank and trace of shared frame tensorsTerminal exceptions from real capacity cutsPrescribed Gram products routed intodistinct retained tester pairsInverse-polynomial tiny-cover compatibilityCounting component tensors with boundedtotal rankFormal forward and reverse rows of a unarymixer testThe finite simultaneous unary mixer estimateJoint distribution of the unary mixer rowmatrixUniform mixing forms chosen simultaneouslybefore any unit lawUniform raw channel phase tails overbounded-rank targetsUniform early channel choice for actualaccepting tablesTerminal containers for actual admissibleunit lawsAdmissible pair lawsWhole-unit conditioned pin avoidanceUniversal protected pin witnessesOrthogonality and finite Walsh correlationboundsWitness atoms and their numerical testerrecords
    Proven claimDefinitionThis submissionA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Proofs

    Proof networkview on GitHub

    100%
    AcceptingFamilies123AcceptingInjection12ActualDeficits123AdaptiveSampling12AdaptiveSets12AffineImages1234AffineSliceIndependence12345678AffineSliceScales12AffineSliceVariance12345AmplifiedTests12AtomDirections123AtomFunctionals1234AtomParameters12345AtomProducts123Atoms123BarredElimination123BarredSpaces123BaseCompression1234567891011121314BaselineRank12BilinearWalsh123456BinaryMixer123456BinaryMixers123BipartiteFlows12345678BlockDeficits123BooleanWeight12345678910BoundedDerivatives1234567CellAveraging12345CellRepresentatives12ChannelAssembly12345ChannelChanges1234567ChannelCharacters123456ChannelColumns123456ChannelDensity1234ChannelFactorization123456789ChannelGroups123ChannelMoments12CoefficientPhase12CollisionCosts123CollisionExponents123456CollisionPruning12345CollisionScales12345CombinedSpans12345CommonAtoms12CommonExactification1234CommonTestTransfer12ComponentCharacters12345ComponentDuals123ComponentMoments12ComponentSpaces1234ComponentTests12CompressedResidual12ConcreteCut12ConcreteGeometry12ConcreteModel12ConditionalChannels1234ConditionalMinus1234ConditionedAffineColumns1234ConditionedMixing123Conditioning12345ConstrainedCompression123456789ContainerAsymptotics12ContainerLaws12345678910ContainerRun12345678CoordinateRestrictions123CorankCounting123Counterexample12CoverAvoidance1234CoverProjection123456CoverSpace12CrossBatchMixing12CrossGramBasis123CutSparsity12345DerivativeContractions1234DerivativeResponses1234567891011DisjointSampling12345DuplicatedMoments12DuplicatedNoCover12DyadicDeficits1234DyadicMoments123DyadicScale12DyadicTails123EffectiveBounds123EffectiveObstructions12345678EmptyPredictions12EntropyContainers123EntropyLines12345EntropyProjection12345EntropySelectors12ExactPins12345FingerprintCounts1234FingerprintScales12345FiniteCollision1234FiniteLinearLaw12345FiniteMoments12FiniteSampling123456FixedSelectorGram123456789FlatRank1234FlavorAffineSlices1234FlowCuts1234567FormalQuadratic123FourPhaseParity12345678FourierTests123456FractionalColoring12FrameExistence12FrameSymmetry12345FrameTranspose123FrameTuples123456FreshKeys12FrozenAssembly123FrozenBaselines12FrozenCellDirections1234FrozenCharacters12FrozenRecords1234FrozenValues12GoodSamples1234GradientAssembly123GramColumns1234GramNormalization1234GramOrbitDensity123GramTests123GraphFailure12GreedySpaces123GreedySpans123456789101112GreedyTails123GroupTensorComparison123HadamardRank12345HistogramGram12345ImageScale1234IndependentMixtures12IndependentSampling12IndependentWitnesses123InjectionAsymptotics123InjectionBudgets123456InjectionThresholds12InjectionUnion123InjectiveDensity123InjectiveFrames12345JoinedGramOrbits123JoinedRecords1234567JointGramInjection123KernelWitness1234KeyMeasures12345KeySpans123LabelRelations123LeafBlockCaps1234LeafCollision12345LeafImages123LeafTrimming1234567ListDeficits12ListTails1234567LowRankCounting123MappedSpans12MatchingCoverage1234MatchingSamples1234567MetadataPins123MixerCompatibility12MixtureRecovery1234MomentBudgets123MomentRecovery12MomentTails12MultiChannelPhase1234NoCoverMoments123NominalPrimal123NonlinearChannels123456789101112OrderedMixerLaw123456PairPositions12PairRecovery123456PairedAnnihilators12PairedFrames12PairedKeys12PairedRecipes123PairedWitnesses123PairingRank12ParameterCellAveraging123PartitionLists123PeelingBudget123PhaseAverages1234PhaseScales12PinLabelExclusions123PinReindexing123PointPrediction12PointQuadratics12PolynomialTensors12PreparedInjection12PrimalAvoidance123456PrimalContractions1234PrimalGramTests1234567PrimalRecords123456ProbabilityScales12ProductImages12345ProductMinusImages12ProfileCounting12ProjectedCoefficients12ProjectedOffsets12ProjectedPins123ProtectedChannels123PureObstructions123PureTesterRoom1234567PushforwardWalsh1234567QuadraticBias1234567QuadraticDegree123QueryRecordBounds1234QueryReference12345QuerySlots12345QuotientCompression12345678QuotientExtractors123QuotientFactorLifts12345678910QuotientFactors123QuotientRank123RankLoss123RankedProjection1234567RawAcceptingInjection123RawBatchComparison12RawCellEntropy12RawContractions123RawFrameComparison1234RawGroupedComparison12RawIntersections12345RawLaw12RawPrimalAvoidance12RawQueryImages1234567RawRetainedCells12RawToGraph12RealCellLaws12345678910RealFlows1234RecipeResiduals12RecipeRows12RecordCollision1234ReferenceImages123ReferenceKeys123RelativeEntropy12345678ResidualFlows1234ResidualLabels12ResidualRealization12345678910ResponseMatrices12345678910111213141516171819ResponseSolvability12345678RestrictedLeaves12RestrictionRank12RetainedCharacters123456RetainedEmptyPredictions123RetainedImages12345RightQueryImages12345SampleScales1234ScalarGramAgreement12SecondPeeling12SelectedBlocks123SelectedMoments12SelectedRemoval123SelectedScalars12345SequentialTests1234567SharedTesterPoint12SharpMixerLaw123456SlotWalsh123SmallSliceRank12345678SmallSubspaceCount12SmallTables12SpanDeficits123SparseIntersections123SparseRepresentatives1234SplitTrimming1234StarRouting123456789101112SumEnvelope123SumRank12SymmetricFactorization12SymmetricPrescriptions123SyntheticGramSlices123SyntheticRankTransfer123456TableCounts123TableInjection12TableSpaces12345TargetMatrices1234567TargetTesters123456789TensorAnnihilators123TensorBlocks12TensorCharacters12TensorContractions1234TensorIntersections1234TerminalCuts123TesterProductRouting123TinyCompatibility12TotalRankCount123UnaryMixer12345678910UnaryMixers1234567UnaryRowLaw1234UniformMixers123UniformPhaseTails12UnitContainers123UnitLaws12345UnitSpanAvoidance123UniversalWitnesses12Walsh12345WitnessAtoms123ActualCellCollisionAdaptiveProtectionAdaptiveUnionBaseMomentsBilinearMeanBinaryPrescriptionsBoundedPeelingChromaticBoundComponentRankGrowthConcreteRecipesConditionalPairsCoordinateCountsCoverClassesCoverCountsCutFunctionalsCutProfilesDirectRanksEmpiricalVarianceExposedSumsFilterOccurrencesFiniteInjectionFixedMultiPhaseFixedNoCoverFourHolesFractionalCounterexampleFrozenGradientsGradientFormGradientRealizationGroupPhaseScaleHoleTriangleFreeIndexedRankGrowthJointDirectionsJointKeyCapJointProjectorsLabelDecompositionLeafCellImagesLeafExtractionLeafPartitionLiftedSumMarkedPhaseMatchingMinorBoundMixerRowLawModeBudgetsMomentIntersectionNoCoverCertificateNoCoverPhaseNoCoverRankNominalBaselinesOrbitSliceLawPaperGraphProbabilityPaperGraphTransferPaperSampleSuccessPreparedInjectionScalePrimalRetractionsProjectedCountsProjectedSpansQueryIndependenceRankFactorsRawBaselinesRawFramesRawJointImagesRawPeelingRawSecondPeelingRecipeChannelsReferencePinsSampledGraphSelectorInterpolationSmallExposureSmallMultiPhaseSmallNoCoverSpanDeficitMonoSparseKeyCoefficientsSparsePinsTableContractionsTagGeometryUniformTableInjection
    assumptions conclusionProven claimStatement 1, 2, … of a claim with several statementsClaim from this submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    No other submission in the archive builds on this one, and this one builds on none.

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-342547,
  author = {Édouard Bonnet and OpenAI and Codex 6.1},
  title = {A counterexample to Hadwiger's conjecture},
  year = {2026},
  howpublished = {Lax Archive, lax-342547},
  url = {https://laxarchive.org/lax-342547/},
  note = {draft},
}

    References

    1. OpenAI. A counterexample to Hadwiger's conjecture. OpenAI Math Release preprint, 2026. github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-counterexample-to-Hadwigers-conjecture-September-23-2026/paper.pdf

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…