ACMaxConjecture/formalization.yaml at main · MerLeanProver/ACMaxConjecture · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
# Repository-level formalization metadata.
# Schema: https://github.com/mathlib-initiative/formalization.yaml

version: "v0.3"

project:
  name: "A complete Lean 4 formalization of the ACMAX conjecture"
  repository: "https://github.com/MerLeanProver/ACMaxConjecture"
  authors:
    - "Zeru Zhu"
    - "Jinzheng Li"
    - "Yuanjie Ren"
  license: "Apache-2.0"

sources:
  - title: "Maximizing algebraic connectivity for certain families of graphs"
    authors:
      - "Theodore Kolokolnikov"
    id: "arXiv:1412.6147v1"
    type: "journal article (preprint on arXiv)"
    journal_ref: "Linear Algebra and its Applications 471 (2015), 122-140"
    doi: "10.1016/j.laa.2014.12.023"
    formalized_from: >-
      Conjecture 1.5. The proof is original rather than a transcription of an
      argument in the source paper.

status:
  scope: >-
    Kolokolnikov's Conjecture 1.5 for every n >= 4. Both the universal upper
    bound and the equality attained by K_{2,n-2} are proved.
  sorry_count: 0
  sorry_in_definitions: 0
  axioms:
    - "propext"
    - "Classical.choice"
    - "Quot.sound"
  main_results:
    - declaration: "ACMax.acmax_conjecture"
      file: "ACMaxConjecture.lean"
      sorry_count: 0
      axioms:
        - "propext"
        - "Classical.choice"
        - "Quot.sound"
      comparator_config: "comparator_config.json"
      literature_dependencies: []
      review: "kernel-checked; associated mathematical proof human-audited"
      note: >-
        The root file has exactly 62 local module dependencies. The active
        closure contains no sorry, admit, or native_decide.

automation:
  methods:
    - method: "autonomous"
      models: []
      framework: "MerLean"
      tool_setup: >-
        MerLean is an autonomous Lean 4 and Mathlib theorem-proving system
        built from language-model agents over a persistent dependency graph.
        Its architecture and evaluation are outside the scope of the
        accompanying mathematical paper.
      cost:
        wall_time: "approximately eighteen days"
        hardware: "API-based agents with local Lean builds"
  notes: >-
    Agent output was treated as untrusted proof search. Declarations were
    accepted only after Lean kernel checks, and numerical certificates were
    cross-checked by exact integer computations before formalization.

fidelity:
  divergences: >-
    ACMax.algConn is defined from Mathlib's sorted Laplacian spectrum, and the
    Courant-Fischer test-vector principle is proved as a bridge theorem. The
    graph vertex type is Fin n. Natural-number subtraction in 2 * (n - 2) is
    harmless under 4 <= n. The Nonempty (Fin n) instance is explicit although
    it follows from 4 <= n.

review:
  status: "mathematical proof human-audited; formal source kernel-checked"
  human_reviewed_scope: >-
    The complete self-contained proof in paper/main.tex, including all order
    ranges, was read manually after being cross-checked against the canonical
    Lean declarations and exact-arithmetic verification scripts.
  not_human_reviewed_scope: >-
    This does not claim that every implementation line in the 62-module Lean
    dependency closure was manually reviewed line by line.
  notes: >-
    The formal assurance consists of successful clean builds, an axiom audit
    of the root theorem, and an independently stated comparator harness.

alignment:
  namespace: "ACMax"
  statements:
    - source: "Conjecture 1.5"
      lean: "ACMax.acmax_conjecture"
      module: "ACMaxConjecture.lean"
      status: "proved"
      note: "The complete conjecture for all n >= 4."
    - source: "Algebraic connectivity"
      lean: "ACMax.algConn"
      module: "ACMaxConjecture/Spectral/AlgConn.lean"
      status: "defined"
    - source: "lambda_2(K_{2,n-2}) = 2"
      lean: "ACMax.algConn_completeBipartite_two"
      module: "ACMaxConjecture/Spectral/AlgConnK2.lean"
      status: "proved"
    - source: "Courant-Fischer upper bound"
      lean: "ACMax.algConn_le_two_of_testvector"
      module: "ACMaxConjecture/Spectral/TestVector.lean"
      status: "proved"

acknowledgements: >-
  Built on Lean 4 and Mathlib. The formalization was generated with MerLean.
  The conjecture is due to Theodore Kolokolnikov.