Razborov의 flag algebra (플래그 대수) 방법은 극단 그래프 이론 (extremal graph theory)에서 점근적 부등식 (asymptotic inequalities)을 증명하는 강력한 도구이며, 종종 이 작업을 준정부호 계획법 (semidefinite programming)을 통해 유한한 증명서 (finite certificate)를 찾는 문제로 환원합니다. 우리는 유한 단순 그래프 (finite simple graphs)에 대한 이 방법의 기계 검증된 정식화 (machine-checked formalization)와 함께, 외부에서 생성된 증명서 데이터를 Lean에 의해 검증되는 대수적 증명으로 변환하는 증명서-증명 컴파일러 (certificate-to-proof compiler)를 제시합니다. 이 정식화는 방법론의 기초를 다룹니다: 부분적으로 라벨이 붙은 그래프 (partially labeled graphs), 큰 그래프에서의 해당 그래프 밀도 (densities), 밀도 표현식의 몫 대수 (quotient algebra), 양의 준동형 사상 (positive homomorphisms)을 통한 그래프 한계 의미론 (graph-limit semantics), 그리고 라벨을 평균화하는 데 사용되는 하향 연산자 (downward operators)를 포함합니다. 컴파일러는 외부의 준정부호 계획법 출력을 신뢰할 수 있는 입력이 아닌 후보 데이터로 취급합니다: Lean은 필요한 밀도 및 곱셈 사실을 독립적으로 계산하고, $\mathbb{Q}$ 위에서 양의 준정부호성 (positive semidefiniteness)을 정확하게 검증하며, flag-algebra 증명의 대수적 정규화 (algebraic normalization) 단계를 수행합니다. 우리의 사례 연구는 Mantel의 정리와 Erdős의 오각형 정리 (Erdős pentagon theorem), 삼각형이 없는 그래프에 대한 $C_4$ 밀도 상한, 그리고 $K_4$-free, $K_5$-free, $C_5$-free 그래프에 대한 에지 밀도 (edge-density) 상한을 포함하여 7가지 Turán 유형 상한에 대한 형식적 증명을 산출합니다. 컴파일러와는 독립적으로, 우리는 Mantel의 정리와 Erdős의 오각형 정리의 정확한 Turán 밀도를 완성하는 일치하는 구성 (matching constructions)을 정식화하고, Goodman의 두 부등식을 증명합니다. 우리의 제약된 의미론 (constrained semantics)은 또한 그래프 제약을 부과하는 두 가지 방식에 대한 메타 이론적 비교를 유도했습니다: 처음부터 flag algebra에 유전적 제약 (hereditary constraint)을 구축하는 방식, 또는 라벨이 무작위로 선택된 제약된 그래프 한계 (constrained graph limits)에서 사후에 부등식을 테스트하는 방식입니다. 우리는 두 접근 방식이 일치하는 시점을 특징짓는 결과적인 root-plantability 기준을 기술합니다; 향후 발표될 논문에서 완전한 설명을 제시할 예정입니다.