🔢 mathematics

Formalizing Flag Algebras in Lean

Dit artikel presenteert een door de machine gecontroleerde formalisering van Razborovs flag-algebra-methode in Lean, met een compiler die certificaten van semidefiniete programmering onafhankelijk verifieert om zeven Turán-type bovengrenzen rigoureus te bewijzen en de metatheoretische nuances van het opleggen van graafrestricties te verkennen.

Oorspronkelijke auteurs: Gyeongwon Jeong, Seonghun Park, Jihoon Hyun, Sang-il Oum, Hongseok Yang

Gepubliceerd 2026-07-28

📖 4 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Gyeongwon Jeong, Seonghun Park, Jihoon Hyun, Sang-il Oum, Hongseok Yang

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een detective bent die een mysterie probeert op te lossen over hoe dingen in elkaar passen. In de wereld van de wiskunde, specifiek een tak genaamd "extremale graaftheorie", is dit mysterie: als je een enorme collectie stippen (vertices) hebt die verbonden zijn door lijnen (edges), en het is je strikt verboden om een specifieke vorm te tekenen—zoals een driehoek of een vierkant—wat is dan het absolute maximum aantal lijnen dat je kunt tekenen voordat je per ongeluk die verboden vorm creëert? Het is alsof je probeert zoveel mogelijk speelgoed in een doos te proppen zonder een kwetsbare vaas in het midden te verbrijzelen. Wiskundigen proberen deze "paklimieten" al decennia lang te vinden, maar de getallen worden zo groot en de patronen zo complex dat menselijke hersenen niet elke mogelijke situatie kunnen controleren.

Om dit aan te pakken, hebben wiskundigen een slimme truc uitgevonden genaamd "flag algebra's". Denk bij een "flag" niet aan een stuk stof aan een mast, maar aan een kleine, gelabelde snapshot van een graaf. Als je een gigantische graaf hebt, is een flag slechts een klein stukje ervan waarbij sommige stippen zijn gemarkeerd met stickers (labels) om bij te houden wie wie is. De methode gebruikt deze kleine snapshots om algebraïsche vergelijkingen op te stellen die de hele gigantische graaf beschrijven. Het is also kind de weersomstandigheden van een heel continent te begrijpen door de windsnelheid te meten op slechts een paar specifieke, gelabelde plekken. Door deze vergelijkingen op te lossen, kunnen wiskundigen strikte bovengrenzen bewijzen voor hoeveel lijnen er kunnen bestaan zonder de regels te breken. Deze bewijzen vertrouwen echter vaak op massale computerberekeningen die te groot zijn voor een mens om met de hand te controleren, wat een knagende twijfel achterlaat: "Heeft de computer een fout gemaakt?"

Dit artikel gaat over het bouwen van een superstrikt, door machines gecontroleerd veiligheidsnet voor deze bewijzen. De auteurs, een team van onderzoekers uit Korea, hebben de volledige theorie van flag algebra's vertaald naar een programmeertaal genaamd Lean, die fungeert als een hyperlogische robotrechter. Ze hebben niet alleen de regels geschreven; ze hebben een "certificate-to-proof compiler" gebouwd. Stel je een scenario voor waarin een computerprogramma (zoals de assistent van een detective) een oplossing vindt en je een stapel papier overhandigt met de tekst: "Hier is het bewijs!" Meestal zou je moeten vertrouwen op het feit dat de computer de wiskunde niet heeft verpest. Maar dit artikel introduceert een systeem waarbij de stapel papier van de computer wordt behandeld als een verdachte. De Lean-compiler neemt die stapel, voert elke enkele berekening vanaf nul opnieuw uit met zijn eigen interne logica, controleert of de "positief semidefiniete matrices" van de computer (een chique manier om te zeggen: gegarandeerd niet-negatieve getallen) daadwerkelijk correct zijn, en assembleert vervolgens een definitief, onbreekbaar bewijs.

Het team heeft dit systeem getest op zeven beroemde wiskundige puzzels, waaronder de stelling van Mantel (over driehoekvrije grafen) en de Erdős-pentagonstelling (over pentagonen in driehoekvrije grafen). Ze hebben er succesvol in geslaagd om deze externe computergegenereerde "certificaten" om te zetten in formele, door machines geverifieerde bewijzen voor alle zeven gevallen. Dit betekent dat we voor deze specifieke problemen nu een wiskundige garantie hebben dat de antwoorden correct zijn, tot op de laatste decimaal, omdat een computer elke stap van de logica heeft geverifieerd. Ze hebben hun nieuwe instrumenten ook gebruikt om enkele ondergrenzen te bewijzen (om aan te tonen dat je deze limieten kunt bereiken) en onderzochten een diepe theoretische vraag over hoe men met de "verboden" vormen in de wiskunde moet omgaan, waarbij ze ontdekten dat de manier waarop je de regels instelt soms belangrijker is dan je denkt. Uiteindelijk lost dit werk niet alleen een paar oude raadsels op; het bouwt een nieuwe, betrouwbare motor die complexe, computerondersteunde wiskunde kan omzetten in ijzersterke, door mensen verifieerbare waarheid.

Technische Samenvatting: Formalisering van Flag Algebra's in Lean

Probleemstelling

Extreme grafentheorie behandelt frequent vragen met betrekking tot de maximale frequentie van een specifiek eindig patroon $F$ in grafen die een verzameling verboden patronen $H$ vermijden. Het bepalen van de asymptotische Turán-dichtheid $\pi(F; H)$ is berucht moeilijk omdat het vereist dat het gedrag van alle voldoende grote $H$ -vrije grafen wordt gecontroleerd. De flag-algebra methode van Razborov biedt een krachtige techniek voor deze setting, waarbij het bewijzen van asymptotische grenzen wordt teruggebracht tot het controleren van een eindig aantal algebraïsche voorwaarden via semidefiniete programmering (SDP).

De praktische toepassing van deze methode rust echter op "kandidaat-certificaten" gegenereerd door externe SDP-solvers (bijv. Flagmatic). Deze certificaten bestaan uit duizenden exacte dichtheidswaarden en rationale positief-semidefiniete (PSD) matrices. Hoewel wiskundig solide, is het verifiëren van deze certificaten met de hand impraktisch, en het vertrouwen op externe software zonder formele verificatie introduceert een gat in de logische bewijsketen. De uitdaging is om een machine-gecontroleerd raamwerk te creëren dat deze externe certificaten kan inzien, de onderliggende eindige combinatorische data (isomorfismen, dichtheden, producten) kan verifiëren, en een formeel bewijs kan produceren binnen een bewijsassistent (Lean) die niet afhankelijk is van de betrouwbaarheid van de externe solver of de handmatige transcriptie van data.

Methodologie

De auteurs presenteren een uitgebreide formalisering van de flag-algebra methode van Razborov in Lean 4, gestructureerd in drie afzonderlijke lagen en een metatheoretisch onderzoek:

1. De Specificatielaag (Wiskundige Fundamenten)

Deze laag formaliseert de abstracte wiskundige definities van flag algebra's voor eindige eenvoudige grafen, nauwlettend volgend de standaardliteratuur.

Definities: Het definieert flag-typen (isomorfieklassen van gelabelde grafen), flags, en de flag-algebra $A_\sigma$ als een quotient van een vrije vectorruimte door expansie-identiteiten (afgeleid van de kettingregel).
Semantiek: Het definieert positieve homomorfismen als afbeeldingen van de algebra naar $\mathbb{R}$ die structuur en niet-negativiteit behouden. De semantische niet-negativiteitsconus $C_\sigma$ wordt gedefinieerd als de verzameling elementen die niet-negatief zijn onder alle dergelijke homomorfismen.
Beperkte Semantiek: In tegen tegenstelling tot traditionele presentaties die de verboden-graaf beperking $H$ in de constructie van de algebra inbouwen, construeert deze formalisering de omgeving-algebra van alle eindige grafen. De $H$ -vrijheid wordt later opgelegd via een "ensemble semantische orde". Deze orde beperkt de positieve homomorfismen tot die welke een dichtheid van nul toekennen aan grafen die $H$ bevatten, gebruikmakend van een willekeurige extensie-maat om ongelijkheden op gelabelde flags te interpreteren.
Downward Operator: Het formaliseert de operator die gelabelde algebra-elementen naar ongelabelde elementen brengt, en bewijst dat deze semantische niet-negativiteit behoudt (Theorema 2.9).

2. De Reflectielaag (Uitvoerbare Berekeningen)

Omdat de specificatielaag rust op niet-berekenbare quotient-typen en abstracte definities, is een aparte "reflectielaag" ontwikkeld om de noodzakelijke eindige berekeningen uit te voeren.

Concrete Representaties: Het gebruikt concrete datastructuren (bijv. Sym2Graph met vertices als Fin n en edges als eindige verzamelingen) om grafen en flags te representeren, wat enumeratie en beslisbare gelijkheid mogelijk maakt.
Adequaatheidstheorema's: De kern van deze laag bestaat uit stellingen die bewijzen dat de uitvoerbare berekeningen (dichtheidsberekeningen, isomorfie-checks, downward normaliserende factoren) overeenkomen met de abstracte definities in de specificatielaag.
Metaprogrammering: Aangepaste elaboratie-tijd commando's genereren specifieke flags, dichtheidstabellen en multiplicatietabellen voor de omvang die vereist is voor een specifiek certificaat. Deze commando's bewijzen volledigheidslemma's die garanderen dat alle relevante isomorfieklassen worden gedekt.

3. De Certificate-to-Proof Compiler

Deze component automatiseert de vertaling van externe SDP-certificaten naar geverifieerde Lean-bewijzen.

Input: Het accepteert een JSON-certificaat van Flagmatic met doelgrafen, verboden grafen, voorgestelde grenzen, flag-typen en rationale PSD-matrices.
Verificatieproces:
1. Regeneratie: Het regenereert de noodzakelijke flags en dichtheid/multiplicatie-identiteiten met behulp van de reflectielaag, in plaats van de data van het certificaat te vertround.
2. PSD Verificatie: Het reconstrueert de rationale matrices en verifieert hun positief-semidefinietheid over $\mathbb{Q}$ met behulp van exacte $LDL^\top$ factorisaties, waarbij floating-point aritmetica wordt vermeden.
3. Algebraïsche Assemblage: Het gebruikt de geverifieerde identiteiten om de algebraïsche identiteit van het certificaat uit te breiden (het decomponeren van de gap $c \cdot 1 - [F]$ in downward vierkanten en een niet-negatieve rest) en controleert de uiteindelijke ongelijkheid.
Vertrouwensmodel: Het compiler-script is onbetrouwbaar; het genereert een bewijs-voorstel. Lean controleert onafhankelijk elke stap, inclusclusief de matrixfactorisaties en de algebraïsche normalisatie. Het script is alleen vertrouwd voor de getrouwheid van de vertaling (het mappen van certificaat-flags naar de Lean-enumeratie), wat controleerbaar is door het gegenereerde stellingverloop te inspecteren.

4. Meta-theorie van Beperkte Semantiek

Het artikel onderzoekt de relatie tussen de "ensemble semantiek" (gebruikt in de implementatie) en de "quotient semantiek" (waar beperkingen ingebouwd zijn).

Root-Plantability: De auteurs definiëren een criterium genaamd "root-plantability" om te karakteriseren wanneer de twee semantische benaderingen overeenkomen. Ze bewijzen dat als een graafklasse "blow-up-closed" is (bijv. $K_r$ -vrije grafen voor $r \ge 3$ ), de twee orden overeenkomen.
Tegenvoorbeeld: Ze leveren een tegenvoorbeeld ( $C_4$ -vrije grafen) waar de orden verschillen, wat aantoont dat hereditairheid alleen onvoldoende is voor overeenkomst.

Belangrijkste Resultaten

De auteurs hebben de compiler geëvalueerd op zeven verschillende upper-bound certificaten, en hebben succesvol machine-gecontroleerde bewijzen geproduceerd voor:

Mantels Stelling: Het bewijzen van $\pi(K_2; K_3) = 1/2$ .
Erdős Pentagoon Stelling: Het bewijzen van $\pi(C_5; K_3) = 24/625$ . (Geen bewijs dat flag algebra's vermijdt is bekend voor dit resultaat).
$C_4$ -dichtheid: Een bovengrens op de dichtheid van $C_4$ in driehoek-vrije grafen.
Edge-density grenzen: Voor $K_4$ -vrije, $K_5$ -vrije, en $C_5$ -vrije grafen.

Daarnaast werd de formalisering direct gebruikt (zonder de compiler) om:

De bijbehorende lower bounds voor Mantels stelling en de Erdős pentagoon stelling te bewijzen met expliciete constructies.
Twee ongelijkheden van Goodman te bewijzen.

Alle zeven certificaten werden gecompileerd naar Lean bronbestanden die geen sorry of axioma's bevatten. Vijf van de zeven werden volledig geverifieerd via kernel reductie (decide +kernel), terwijl de twee grootste ( $K_5$ -vrije en $C_5$ -vrije edge density) natuurlijke decide vereisten vanwege computationele limieten, een beperking die de auteurs expliciet erkennen.

Betekenis en Claims

Het artikel claimt de eerste machine-gecontroleerde formalisering van de flag-algebra methode voor eenvoudige eindige grafen te bieden, waarmee de kloof tussen computer-ondersteunde zoektocht en rigoureus formeel bewijs wordt overbrugd. De betekenis ligt in:

Verificatie van Complexe Combinatoriek: Het demonstreert dat flag-algebra bewijzen, die rusten op enorme hoeveelheden exacte eindige data en SDP-resultaten, volledig geverifieerd kunnen worden in een bewijsassistent zonder de externe solver of handmatige transcriptie te vertrouwen.
Modulaire Architectuur: De scheiding tussen de specificatielaag (wiskunde), de reflectielaag (computatie) en de compiler-laag (automatisering) biedt een herbruikbaar raamwerk voor het formaliseren van andere extreme problemen.
Meta-theoretisch Inzicht: De formalisering van de ensemble semantiek en het root-plantability criterium biedt een rigoureuze wiskundige verstandhouding van de beperkingen die de implementatie oplegt, wat verheldert wanneer de "random-label" benadering gelijk is aan de "built-in constraint" benadering.
Nieuwe Bewijzen: Het levert het eerste formele bewijs van de Erdős pentagoon stelling en nieuwe formele bewijzen voor de Goodman ongelijkheden en de lower bounds voor Turán-dichtheden.

De auteurs blijven bescheiden over de huidige beperkingen en merken op dat de aanpak afhankelijk is van externe SDP-solvers voor het ontdekken van certificaten en dat het schalen voorbij vijf vertices momenteel aanzienlijke computationele hindernissen voor kernel-gecontroleerde verificatie met zich meebrengt. Zij beschouwen dit werk als een fundament voor toekomstige uitbreidingen naar hypergrafen, gerichte grafen, en de integratie van graphon theorie.