Auto-Formalizing Theoretical Domains

Disproved. Socially optimal cut colorings can fail to be strong equilibria

Partial. Conjectured wild number formula proved for all large complete graphs

Proved. Exact counting formula proved for Latin tableaux with double-three tails

Proved. No integer square admits a perfect rectangle tiling of two-prime area

Disproved. Universal spectral bound fails for positive trace-preserving maps in dimension three

Lean accepted 1510 new theorems this week, drawn from 97 papers and 23 topics. Of these, 53 are new here, 0 correct a published claim, 150 formalize a published result and 1307 are helper lemmas. They make 14 research-level results, in 16 theorems -- they lead the report. 1276 statements posed this week are not yet proved. The reading covered 109 new papers. This report covers 16 results in 6 fields.

The Proposer read 0 new paper(s) and listed 0 open problem(s); 16 new question(s) of AFTD's own were adopted onto the list; 9 list entries were stated in Lean, as were 10 results the papers prove; the Proposer posed 37 more from what the knowledgebase already holds (270 new theorem statement(s) in all, each checked against its English in both directions). The Prover proved 167 theorem(s), 135 of them helper lemmas, which are not listed below; 118 of today's statements are not yet proved and stay in the knowledgebase, marked as such.

Research-level. not_universal_spectral_bound_positive_trace_preserving (arXiv:2610.37187): Not every positive trace-preserving linear map on d × d complex matrices with d ≥ 3 satisfies Tr(Φ) ≤ d m(Φ) + d² − d: in dimension 3 the positive trace-preserving map X ↦ K X K + (3/4) P Xᵀ P, K = diag(1/2, 1/2, 1), P = diag(1, 1, 0), has operator trace… — (medium tier) Answers the question left open in arXiv:2610.37187 (Sec. 9) and raised in arXiv:2506.02145: positive trace-preserving maps in dimension three can violate the universal spectral bound Tr Φ ≤ d m(Φ) + d² − d that holds for all 2-positive ones; an explicit decomposable map with trace 11/2 and eigenvalue −1/2 exceeds the bound 9/2

Research-level. exists_positive_tp_violating_universal_spectral_bound (arXiv:2610.37187): For every d ≥ 3 there is a positive trace-preserving linear map Φ on d × d complex matrices with Tr(Φ) > d m(Φ) + d² − d. With a = (d−2)/(d−1), K = diag(a, a, 1, …, 1) and P the diagonal projection onto the first two coordinates, Φ(X) = K X K + (1 − a²) P Xᵀ… — (medium tier) Answers the question of arXiv:2610.37187 (Sec. 9, raised in arXiv:2506.02145) in every dimension: for each d ≥ 3 an explicit decomposable positive trace-preserving map violates the bound Tr Φ ≤ d m(Φ) + d² − d, which holds for all 2-positive trace-preserving maps, by 2/(d − 1); so 2-positivity cannot be weakened to positivity in that theorem

Research-level. efx_exists_of_two_universal_small_goods_ir (arXiv:2208.08782): Let m and n be natural numbers with n positive. There are m+2 goods with nonnegative real additive values for n agents. Each agent values each of the last two goods no more than every one of the first m goods, with no required order between the last two.… — (low tier) Extends common least-good insertion to two universally small goods with arbitrary within-pair rankings, preserving every old bundle and weakly improving all own utilities; iteration gives complete EFX for any number of agents and goods ordered in common pairs

Partial result on OP-651. cyclic_cubic_t_count_isotropy_lower_bound (knowledgebase): For every natural number n ≥ 6 and every finite set S : Finset (Finset (Fin n)), if is_parity_repr S (cyclic_cubic_syndrome n), then 2 * n + 1 ≤ S.card.

Partial result on OP-666. three_token_k2n_domination_number_four (knowledgebase): The domination number of the 3-token graph F_3(K_{2,4}) of the complete bipartite graph K_{2,4} is 4.

Partial result on OP-736. ghz_network_lambda_standard_frame (arXiv:2610.35838): For the generalized GHZ state with parameter alpha, the identity frames e = I and f = I at indices (3, 0) and (1, 1) satisfy Lambda(tau_{30}, tau_{11}) = 1 + sin^2(2*alpha).

Partial result on OP-736. ghz_two_copy_closed_lower_bound (arXiv:2610.35838): For every parameter alpha, there exist orthonormal frames e and f in O(3) and setting indices mu, nu, mu', nu' in {0, 1, 2, 3} such that the two-copy closed-network quantity Lambda(tau_{mu nu}, tau_{mu' nu'}) equals 1 + sin^2(2*alpha).

Partial result on OP-735. dichotomic_sum_diff_sq_sum (arXiv:2610.35838): For any two dichotomic projective observables B_0, B_1 on a Hilbert space, (B_0 + B_1)^2 + (B_0 - B_1)^2 = 4 I.

Partial result on OP-716. fourier_threshold_nu_odd_ge_arithmetic_bound (arXiv:2610.38447): For every integer m >= 1, the arithmetic bound lambda_{2m+1} is a lower bound on the Fourier threshold nu(2m+1).

Partial result on OP-716. fourier_threshold_nu_one (arXiv:2610.38447): The Fourier threshold nu(1) for functions from ZMod 2 to ZMod 3 with unique zero at 0 is equal to 2.

Partial result on OP-716. fourier_threshold_nu_two (arXiv:2610.38447): The Fourier threshold nu(2) for functions from (ZMod 2)^2 to ZMod 3 with unique zero at 0 is equal to 3.

Formalized. observable_upper_bound_base_polytope (arXiv:2610.35433 Corollary 1 proof): For any vector a whose values are sorted non-decreasingly by permutation π, and any point z in the base polytope of C, the inner product ∑ i, a i * z i is bounded by a(π(0)) + ∑_{k=0}^{n-2} (a(π(k+1)) - a(π(k))) * C(S_{k+1}).

Formalized. anticommuting_hermitian_expectation_sq_le_one (arXiv:2610.35838 Appendix E, Fact 1): If continuous linear operators P and Q on a complex Hilbert space are self-adjoint, have operator norm at most one, and anticommute (P * Q + Q * P = 0), then for any unit vector psi, the sum of the squares of the real expectation values satisfies (re <psi, P…

Formalized. concave_power_sum_le (arXiv:2610.35838 Appendix E, Fact 2): For non-negative real numbers p and q such that p^2 + q^2 <= 1, and any real r with 0 < r <= 1, the sum of powers satisfies p^r + q^r <= 2^(1 - r / 2).

Formalized. open_network_kernels_anticommute (arXiv:2610.35838 Appendix E, Eq. (61)): In any ring, dichotomic observables A_0, A_1 and B_0, B_1 squaring to 1 that commute with each other yield anticommuting kernel operators: (A_0 * B_0 - A_1 * B_1) * (A_0 * B_1 + A_1 * B_0) + (A_0 * B_1 + A_1 * B_0) * (A_0 * B_0 - A_1 * B_1) = 0.

Formalized. parity_effect_quantum_network_bounds (arXiv:2610.35838 Theorem 4): For every natural number n with 1 <= n, and all real numbers p, q with 0 <= p, 0 <= q, p <= 1, and q <= 1, if ¬ Even n implies p^2 + q^2 <= 1, then Real.sqrt (p ^ (2 / (n : ℝ)) + q ^ (2 / (n : ℝ))) ≤ closed_network_bound n and p ^ (1 / (n : ℝ)) + q ^ (1 / (n…

Formalized. mixture_representation_monotone_distribution (arXiv:2610.01563 Lemma 3): Let $P : \mathbb{N}^+ \to \mathbb{R}$ be a nonincreasing probability distribution on the positive integers, so that $P(k) \ge 0$ for all $k$, $P$ is antitone, and $\sum_{k=1}^\infty P(k) = 1$. Then the mixture weights $w_k = k(P(k) - P(k+1))$ satisfy: $w_k…

Formalized. dual_melas_non_degenerate_orbit_shift_equiv_iff (arXiv:2610.38017 Lemma 5): Let k ≥ 3, let F be a finite field of order 2^k, and let α ∈ F be primitive of order 2^k - 1. For binary polynomials f and g such that f is non-degenerate (neither α nor α⁻¹ is a root of f), f and g are shift-equivalent modulo the product of the minimal…

Formalized. grid_arrangement_column_deviation_subset_sum_bound (arXiv:2610.38386 Lemma 3.8): Let $n \ge 3$, $N = n^2$, and let $S : \mathrm{Fin}\ n \times \mathrm{Fin}\ n \to \mathbb{Z}$ be an injective arrangement with entries in $\{1, \dots, N\}$. For the column-deviation vector $\gamma_j = \sum_{i=0}^{n-1} S(i,j) - n(N+1)/2$ and any subset of…

Corrected. not_simple_graph_diam_le_two_mul_div_add_one_of_dist_two_transport_bound: The statement simple_graph_diam_le_two_mul_div_add_one_of_dist_two_transport_bound is false: The statement is false due to truncated natural number subtraction k - c : ℕ in the hypothesis hbound. Specifically, if c > 2 * k (e.g. k = 2, c = 5),…

Corrected. not_antipodal_hellinger_majority_three_ratio: The statement antipodal_hellinger_majority_three_ratio is false: The theorem statement claims that dictator_dist 3 majority_three = 1 / 4. However, dictator_dist n f is defined as `⨅ (g : (Fin n → Bool) → ℝ) (_ : is_signed_dictator n g), (1 / (2 : ℝ) ^ n)…

Open. open_problem_736 (arXiv:2610.35838 Sec. III.4): For every parameter alpha in (0, pi/2), all orthonormal frames e, f in O(3), and all setting indices mu, nu, mu', nu' in {0, 1, 2, 3}, the two-copy closed-network Bell measurement quantity Lambda(tau_{mu nu}, tau_{mu' nu'}) for the generalized GHZ state…

Open. magic_rectangle_algebraic_sos_identity: Let A be an ℝ-algebra and let D, C, B : Fin 3 → A satisfy D j ^ 2 = C j ^ 2 = B j ^ 2 = 1 for all j, D 0 * D 1 * D 2 = 1, C 0 * C 1 * C 2 = -1, pairwise commutativity within D and within C, and every D and C commuting with every B. Setting X j = D j + C j, Y…

Open. magic_rectangle_sos_certificate (arXiv:2610.12001 Theorem 3.1): Let H be a complex Hilbert space and let D, C, B : Fin 3 → (H →L[ℂ] H) be self-adjoint continuous linear operators satisfying D j ^ 2 = 1, C j ^ 2 = 1, and B j ^ 2 = 1 for all j, D 0 * D 1 * D 2 = 1, C 0 * C 1 * C 2 = -1, D j * D k = D k * D j, C j * C k = C…

Open. universal_spectral_bound_positive_trace_preserving (arXiv:2610.37187): For every integer d ≥ 3, every positive trace-preserving linear map Φ on d × d complex matrices satisfies the universal spectral bound Tr(Φ) ≤ d * m(Φ) + d^2 - d, where Tr(Φ) is the real part of the operator trace of Φ and m(Φ) is the minimum real part of an…

Open. pocket_depth_bound_from_omitted_max_types (arXiv:2610.37940 Theorem 16): Let B be a finite set of nonempty permutations of natural numbers from 1 to their length. If B contains no pattern whose maximum entry is at the leftmost position, or contains no pattern whose maximum entry is at the rightmost position, then every B-avoiding…

Open. op716_fourier_threshold_odd_eq_arithmetic_bound (arXiv:2610.38447): Open Problem OP-716: for every integer m >= 1, the Fourier threshold nu(2m+1) of functions from (ZMod 2)^(2m+1) to ZMod 3 with unique zero at 0 equals the arithmetic bound lambda_{2m+1}.

Disproved. Unweighted Max-3-Cut games can fail to admit any optimal strong equilibrium

Proved. Line cubic quantum syndrome has exact size 2n + 1 parity representation

Proved. Latin tableaux with double-three tail numbered by closed formula

Partial. Squares have no perfect partitions with two-prime tile areas

Lean accepted 3307 new theorems this month so far, drawn from 205 papers and 34 topics. Of these, 198 are new here, 8 correct a published claim, 484 formalize a published result and 2617 are helper lemmas. They make 17 research-level results, in 20 theorems -- they lead the report. 1808 statements posed this month are not yet proved. The reading covered 330 new papers. This report covers 8 results in 6 fields.

The Proposer read 0 new paper(s) and listed 0 open problem(s); 0 new question(s) of AFTD's own were adopted onto the list; 10 list entries were stated in Lean, as were 8 results the papers prove; the Proposer posed 36 more from what the knowledgebase already holds (83 new theorem statement(s) in all, each checked against its English in both directions). The Prover proved 79 theorem(s), 30 of them helper lemmas, which are not listed below; 26 of today's statements are not yet proved and stay in the knowledgebase, marked as such.

Research-level. power_divergence_exists_binary_counterexample_of_lt_golden_ratio (knowledgebase): For every exponent beta in (0, (sqrt 5 - 1)/2), there exist strictly positive binary probability mass functions pX, PY, PZ forming a Markov chain Y <- X -> Z such that mutual power-divergence information subadditivity strictly fails. — (medium tier) Proves the failure half of the golden-ratio conjecture OP-726 for every exponent, not just at sample points: for every beta in (0, (sqrt 5 - 1)/2) there is a strictly positive binary Markov chain Y <- X -> Z on which mutual power-divergence information is strictly superadditive. The construction is a rare input symbol of probability p and a channel entry of order p, and the slack has derivative -(1-beta)a^2 - (1-(1-a)^beta)^2 + 2 kappa^beta((a+kappa)^(1-beta) - (kappa+a-a^2)^(1-beta)) at p = 0, positive for suitable a, kappa exactly when beta^2 + beta < 1. The source paper (arXiv:2610.21231) gives only sufficient conditions for subadditivity, and the knowledgebase had refutations only at beta = 1/4 and 1/2 plus numerical evidence for the threshold

Research-level. op744_dice11_has_directed_cycle_ge_twelve (arXiv:2610.40321): There exists an integer k ≥ 12 such that has_directed_cycle (dice_graph 11).Adj k holds. — (low tier) settles OP-744 (Existence of a non-transitive cycle of length at least 12 for 11-sided dice)

Partial result on OP-161. cycle_seven_all_powers_well_covered (arXiv:2610.09300): For every positive integer d, the d-th power of the 7-cycle graph C_7 is well-covered.

Partial result on OP-537. exists_planar_all_powers_well_covered_diam_eq_three (knowledgebase): There exists a finite connected simple planar graph G with at least two vertices whose diameter is exactly 3 and such that every positive integer power G^d (for d ≥ 1) is well-covered.

Partial result on OP-538. bipartite_all_powers_well_covered_diameter_le_two (knowledgebase): Every finite connected bipartite simple graph G with at least two vertices whose positive integer powers G^d (for d ≥ 1) are all well-covered has diameter at most 2.

Partial result on OP-593. cycle_not_proportionally_two_choosable (knowledgebase): For every integer n ≥ 3, the simple n-cycle C_n is not proportionally 2-choosable: it is not the case that for every finite color palette α and every assignment L of 2 colors to each vertex, there exists a proper coloring f of C_n with f(v) ∈ L(v) for all v…

Partial result on OP-726. mutual_power_divergence_not_subadditive_of_lt_golden_ratio (knowledgebase): For every exponent beta in (0, (sqrt 5 - 1)/2), the mutual power-divergence information with generator f_beta fails to be subadditive under Markov chains Y <- X -> Z.

Partial result on OP-729. op_729_case_n_two (knowledgebase): For every Boolean function f : (Fin 2 → Bool) → Bool on 2 variables, optimalTorusError f 0 = predictedTorusError 2 f and HasRationalTorusApproximation f 0 (predictedTorusError 2 f).

Partial result on OP-719. yang_mills_residual_root_m3 (knowledgebase): The rational residual polynomial yang_mills_residual_polynomial 3 evaluated at the rational number 1/21 equals 0.

Partial result on OP-786. min_avg_pairwise_hamming_dist_density_one_sixteenth_n_eq_four (arXiv:2610.40486): For $n = 4$, every subset $F \subseteq (\mathrm{Fin}\ 4 \to \mathrm{Bool})$ of cardinality $2^{4-4} = 1$ attains average pairwise Hamming distance $(4-4)/2 = 0$ and is a $0$-dimensional subcube is_subcube (4 - 4) F.

Thread RT-1. cycle_power_dyadic_class_weight_congr: The dyadic class weight cycle_power_dyadic_class_weight m b depends only on the values b i for i < 2^m: if b i = b' i for every i < 2^m, the two weights are equal.

Thread RT-1. cycle_power_dyadic_no_island_of_alternating_paired: Uniform induction step for the no-island class shape. Let m ≥ 1 and suppose every tight, exactly dyadically covered, fully ordinarily covered integer Boolean class model at exponent m with exactly m+1 active classes at each vertex has no island (a < b < c <…

Thread RT-1. simple_graph_equivalence_covering_number_cycle_power_two_pow_even_not_dvd_of_alternating_paired: Conditional resolution of OP-205: if, for every m ≥ 5, every tight, exactly dyadically covered, fully ordinarily covered integer Boolean class model at exponent m with exactly m+1 active classes per vertex has the alternating-paired structure (x (p+1) 1 =…

Thread RT-1. cycle_power_dyadic_tight_class_inner_imp_one: For m ≥ 2 and a tight dyadic class b : ℕ → Bool at exponent m (class weight equal to class size) with b 1 = b (2^m - 2) and b (2i) = b (2i+1) whenever 1 ≤ i and i + 1 < 2^(m-1): every inner bit forces bit 1, i.e. if 0 < j < 2^m - 1 and b j = true then b 1 =…

Thread RT-1. cycle_power_dyadic_alternating_paired_of_pairing: For m ≥ 2, a tight, exactly dyadically covered integer Boolean class model x : ℤ → ℕ → Bool at exponent m with x p 1 = x p (2^m - 2) for every p and the pairings x p (2i) = x p (2i+1) for 1 ≤ i, i + 1 < 2^(m-1), has the alternating-paired structure: x (p+1)…

Formalized. subdivided_k33_line_graph_isk4_diamond_free_four_chromatic (arXiv:2610.32404 Proposition 11.2, with H as constructed in Section 11.): Let H be the graph obtained from K3,3 by subdividing one edge exactly once, and let G be its line graph. Then G has no induced subdivision of K4, has no induced diamond, and has chromatic number exactly four.

Formalized. cylinder_construction_distance_set (arXiv:2610.34758 Lemma 2.3 -- Geometric progressions in distance sets in odd dimensions over prime fields): Let $p$ be an odd prime (with $p$ prime and $p$ odd) and let $m \ge 0$ be a natural number. There exist an $m$-dimensional submodule $W \le (\mathbb{Z}/p\mathbb{Z})^{2m+1}$ that is totally isotropic with respect to $Q_{2m+1}$ and a vector $e \in…

Formalized. finite_bi_algebra_is_semigroup_with_left_units (arXiv:2610.37108 Proposition 3.1): Every finite BI-algebra is a semigroup with B and I as left units: let (A, ·) be a finite magma equipped with elements B, I in A such that B is a B-element (((Bx)y)z = x(yz) for all x, y, z in A) and I is an I-element (Ix = x for all x in A). Then the binary…

Formalized. tournament_not_king_of_covered (arXiv:2610.40521 Observation 4): If a vertex w covers another vertex v in a tournament T (that is, w -> v and w -> x for every out-neighbor x of v), then v is not a king in T.

Formalized. tournament_is_king_of_max_outdegree (arXiv:2610.40521 Equation 2): In every tournament on n vertices, every vertex of maximum outdegree is a king: every other vertex is reachable from it by a directed path of length at most two.

Formalized. tournament_exists_covering_realization (arXiv:2610.40521 Lemma 6): Let d be a realizable degree vector of an n-vertex tournament, and let v, w be vertices satisfying d v < d w. Then there exists a tournament T realizing d in which w covers v (that is, w -> v and w -> x for every out-neighbor x of v).

Formalized. tournament_universal_kings_iff_max_outdegree (arXiv:2610.40521 Corollary 7): For every realizable degree vector d of an n-vertex tournament and every vertex v, v is a king in every tournament realizing d if and only if v has maximum outdegree according to d (that is, d u ≤ d v for all vertices u).

Formalized. tournament_directed_cut_eq_of_outdegrees_eq (arXiv:2610.40521 Lemma 2: Directed Cut-Query Complexity of Finding a King): Let T₁ and T₂ be tournaments on vertex set Fin n such that every vertex v has the same outdegree in T₁ and T₂. Then for every subset S ⊆ Fin n, the number of edges directed from S to its complement in T₁ equals that in T₂.

Open. yang_mills_additional_root_distinct_explicit (knowledgebase): For every natural number m ≥ 12, with d = 2m + 5, b_coeff = -2*(d^3 - 16*d^2 + 89*d - 146)/((d - 2)*(d - 1)^2), and c_coeff = ((d - 10)*(d - 5)/((d - 2)*(d - 1)))^2, let Q be the monic quadratic polynomial X^2 + b_coeff * X + c_coeff; if a real number z…

Open. min_avg_pairwise_hamming_dist_density_one_sixteenth (arXiv:2610.40486): Let $n \ge 4$ be a natural number. For any subset $F \subseteq (\mathrm{Fin}\ n \to \mathrm{Bool})$ of cardinality $2^{n-4}$, the average pairwise Hamming distance avg_pairwise_hamming_dist F is at least $(n-4)/2$, and equality holds if and only if $F$ is…

Open. subcube_avg_pairwise_hamming_dist (arXiv:2610.40486): For any $n \ge 4$, every $(n-4)$-dimensional subcube $F \subseteq (\mathrm{Fin}\ n \to \mathrm{Bool})$ of cardinality $2^{n-4}$ has average pairwise Hamming distance equal to $(n-4)/2$.

Open. op_776_explicit_polynomial_hitting_small_char (arXiv:2610.37677): There exist constants C, k : ℕ such that for all natural numbers m ≥ 1, S ≥ 1, and every prime p ≤ ((m+2)S choose 2), for every field F of characteristic p, there exist a matrix order R ≤ C * (m + S)^k and a tuple of matrices T : Fin m → Matrix (Fin R) (Fin…

Open. op_776_char_two_hitting_point (arXiv:2610.37677): There exist constants C, k : ℕ such that for all natural numbers m ≥ 1, S ≥ 1, and every field F of characteristic 2, there exist a matrix order R ≤ C * (m + S)^k and a tuple of matrices T : Fin m → Matrix (Fin R) (Fin R) F such that T is an ncABP hitting…

Open. graph_interval_index_path_graph (arXiv:2610.39966 Theorem 5): For every n ≥ 1, the interval index of the path graph P_n equals (n^3 - n) / 6.

The Proposer read 56 new paper(s) and listed 71 open problem(s); 59 new question(s) of AFTD's own were adopted onto the list; 18 list entries were stated in Lean, as were 11 results the papers prove; the Proposer posed 38 more from what the knowledgebase already holds (205 new theorem statement(s) in all, each checked against its English in both directions). The Prover proved 189 theorem(s), 139 of them helper lemmas, which are not listed below; 43 of today's statements are not yet proved and stay in the knowledgebase, marked as such.

Research-level. simple_graph_equivalence_covering_number_cycle_power_fifteen_of_not_dvd (arXiv:2610.15635): For every even n ≥ 3825 = 15²·17 not divisible by 16, the equivalence covering number of the 15th power of the n-cycle is 6 = 2 + ⌈log₂ 16⌉. This settles the case k = 15 (m = 4) of the open problem: the paper's Theorems 1.3-1.4 leave eq(C_n^15) ∈ {5, 6} open… — (medium tier) Settles the k = 15 case of the residual even case of arXiv:2610.15635: eq(C_n^15) = 6 for every even n ≥ 3825 with 16 ∤ n, where the paper only has eq(C_n^15) ∈ {5, 6}; the first case beyond k = 3 where the exact value is now known

Research-level. simple_graph_equivalence_covering_number_cycle_power_seven_of_not_dvd (arXiv:2610.15635): For every n ≥ 98 not divisible by 8, the equivalence covering number of the 7th power of the n-cycle is 5 = 2 + ⌈log₂ 8⌉. This settles the case k = 7 (m = 3) of the open problem: for even n ≥ 441 not divisible by 8 the paper's Theorems 1.3-1.4 only give… — (medium tier) Settles the k = 7 case of the residual even case of arXiv:2610.15635: eq(C_n^7) = 5 for every n ≥ 98 with 8 ∤ n, where the paper only has eq(C_n^7) ∈ {4, 5} for even n ≥ 441

Partial result on OP-601. four_cycle_graph_code_density_tendsto_one_along_powers_of_two (knowledgebase): As the natural number r tends to infinity, the sequence ((2 : ℝ) ^ r) * kst_code_max_density 2 2 (2 ^ r) tends to 1.

Partial result on OP-641. edge_geodesic_transversal_number_corona_k1_card_two (arXiv:2610.36821): For every finite type V with Fintype.card V = 2 and every connected simple graph G on V, the edge geodesic transversal number of the corona product corona_k1 G satisfies edge_geodesic_transversal_number (corona_k1 G) = 1.

Partial result on OP-665. thue_morse_word_length (knowledgebase): For every natural number n, the length of the n-th Thue-Morse word t_n is 2^n.

Partial result on OP-665. thue_morse_random_attractor_prob_zero (knowledgebase): For every natural number n, thue_morse_random_attractor_prob n 0 = 0.

Partial result on OP-605. cycle_graph_six_book_ramsey_witness (arXiv:2610.36522): In the 6-cycle graph on Fin 6, every pair of adjacent vertices has at most 0 common neighbors, and every pair of distinct non-adjacent vertices has at most 1 common neighbor in the complement graph.

Partial result on OP-605. book_ramsey_b1_b2_graph_exists (arXiv:2610.36522): There exists a simple graph G on 6 vertices with decidable adjacency such that every pair of adjacent vertices has at most 0 common neighbors in G, and every pair of distinct non-adjacent vertices has at most 1 common neighbor in the complement graph Gᶜ.

Partial result on OP-561. online_ef1_approximation_ratio_nonneg (arXiv:2610.34625): For any number of agents n, the online EF1 approximation ratio under exact frequency predictions is nonnegative.

Partial result on OP-639. op_639_exists_intersecting_four_uniform_covering_four_card_ge_forty_two (arXiv:2610.37315): There exists an intersecting 4-uniform hypergraph on the natural numbers with covering number 4 having at least 42 edges.

Thread RT-1. cycle_power_fifteen_tight_type_sequence_shape_rules_core_v30_41: Window refutation for k = 15: in the layer-free tight-class model on the integer line (x p j: the class starting at p contains p + j; inner count 3 per vertex, distances 14, 12, 8 covered exactly once, the other distances covered, classes closed under the…

Thread RT-1. cycle_power_fifteen_tight_type_sequence_shape_rules_core_v40_51: Window refutation for k = 15: in the layer-free tight-class model on the integer line (x p j: the class starting at p contains p + j; inner count 3 per vertex, distances 14, 12, 8 covered exactly once, the other distances covered, classes closed under the…

Thread RT-1. cycle_power_fifteen_tight_type_sequence_shape_rules_core_v50_61: Window refutation for k = 15: in the layer-free tight-class model on the integer line (x p j: the class starting at p contains p + j; inner count 3 per vertex, distances 14, 12, 8 covered exactly once, the other distances covered, classes closed under the…

Thread RT-1. cycle_power_fifteen_tight_type_sequence_shape_rules_core_v60_71: Window refutation for k = 15: in the layer-free tight-class model on the integer line (x p j: the class starting at p contains p + j; inner count 3 per vertex, distances 14, 12, 8 covered exactly once, the other distances covered, classes closed under the…

Thread RT-1. cycle_power_fifteen_tight_type_sequence_shape_rules_core_v81_90: Window refutation for k = 15: in the layer-free tight-class model on the integer line (x p j: the class starting at p contains p + j; inner count 3 per vertex, distances 14, 12, 8 covered exactly once, the other distances covered, classes closed under the…

Thread RT-1. cycle_power_fifteen_tight_type_sequence_shape_rules_core_v91_100: Window refutation for k = 15: in the layer-free tight-class model on the integer line (x p j: the class starting at p contains p + j; inner count 3 per vertex, distances 14, 12, 8 covered exactly once, the other distances covered, classes closed under the…

Formalized. seidel_matrix_codegree_eq (arXiv:2610.36522 Lemma 7): For any simple graph G on a finite vertex set V with Seidel matrix S and any pair of adjacent vertices u and v in G, four times the number of common neighbors of u and v equals |V| - 4 - ∑_k S_{uk} - ∑_k S_{vk} + (S^2)_{uv}.

Formalized. seidel_matrix_compl_codegree_eq (arXiv:2610.36522 Lemma 7): For any simple graph G on a finite vertex set V with Seidel matrix S and any pair of adjacent vertices u and v in the complement Gᶜ, four times the number of common neighbors of u and v in Gᶜ equals |V| - 4 + ∑_k S_{uk} + ∑_k S_{vk} + (S^2)_{uv}.

Formalized. admissible_card_sq_add_five_le (arXiv:2610.34372, Lemma 2.1): If A is a nonempty admissible subset of {1, ..., N}, then the square of the cardinality of A plus 5 is at most 6 times N.

Formalized. admissible_card_le_nat_sqrt (arXiv:2610.34372, Lemma 2.1): If A is a nonempty admissible subset of {1, ..., N}, then the cardinality of A is at most the integer square root of 6 times N.

Formalized. recurrence_b_transition_bijective_and_orbit_periodic_and_unique_fixed_point (arXiv:2610.34300 Proposition 7): For any integer k ≥ 2, the transition map of recurrence (B) on (ℤ/3ℤ)^k is bijective, every orbit is purely periodic (for every state w, there exists m > 0 such that the m-th iterate of the map on w is w), and the zero state is the unique fixed point of the…

Formalized. eefx_imp_approx_efk (arXiv:2610.34625 Lemma 3.2 -- Online Fair Division with Frequency Predictions): Let n ≥ 3 and let σ be an allocation of m goods among n agents with nonnegative additive valuations u such that every agent's bundle is nonempty. If σ is an EEFX allocation, then σ is a 1/(n-1)-EF(n-2) allocation.

Formalized. petersen_colorable_of_three_edge_colorable (arXiv:2610.35794 (Computational complexity of the H-coloring problem in cubic graphs), Sec. 3 (H-coloring for 3-edge-colorable H reduces…): If es is an edge list with edge_list_connected_cubic n es that has a proper 3-edge-coloring c : Fin es.length → Fin 3 (any two distinct edges i ≠ j sharing an endpoint get different colors), then it has a Petersen coloring: edge_list_h_colorable…

Formalized. kst_code_linear_construction_finite_field (arXiv:2610.35136 Lemma 4.2): Let n, s, t, r ≥ 1 be integers, and let w_1, ..., w_n in (ZMod 2)^r be vectors such that the sum of w_i over S is nonzero for every subset S of [n] with |S| in {s, t}. Then there exists a binary linear K_{s,t}-code C in the set of simple graphs on Fin n of…

Corrected. not_not_isContained_book_graph_of_commonNeighbors_le: The statement not_isContained_book_graph_of_commonNeighbors_le is false: The statement is FALSE for k = 0. Under Lean's Nat subtraction, 0 - 1 = 0. When k = 0, the hypothesis h requires that every pair of adjacent vertices u, v in G has at most 0 - 1 =…

Corrected. not_card_fiber_one_eq_one: The statement card_fiber_one_eq_one is false: The statement is false. The hypotheses require |A| = |P| + 1, f(A) ⊆ {c0} ∪ P, and that every c ∈ P has at least one preimage in A. However, there is no hypothesis requiring c0 to have any preimage in A.…

Open. radius_independence_connectivity_hamiltonian_interpolation (knowledgebase): Every finite simple graph G on at least three vertices with vertex connectivity kappa(G) >= 2 and independence number alpha(G) <= kappa(G) + rad(G) - 2 contains a Hamilton cycle.

Open. radius_independence_connectivity_hamiltonian_radius_two (knowledgebase): Every finite simple graph G on at least three vertices with vertex connectivity kappa(G) >= 2, radius 2, and independence number at most kappa(G) contains a Hamilton cycle.

Open. thue_morse_random_attractor_lattice_gumbel (knowledgebase): The sequence in n of the supremum over all k in ℕ of |thue_morse_random_attractor_prob n k - Real.exp (-8 * (n : ℝ) * (5 / 6 : ℝ) ^ k)| tends to 0 as n tends to infinity (in Filter.atTop and nhds 0).

Open. op_605_ramsey_b63_b64_graph_exists (arXiv:2610.36522): There exists a simple graph G on 254 vertices with decidable adjacency such that every pair of adjacent vertices has at most 62 common neighbors in G, and every pair of distinct non-adjacent vertices has at most 63 common neighbors in the complement graph Gᶜ.

Open. amply_regular_icosahedron_cartesian_power (arXiv:2610.36620 Theorem 3.6 -- Diameter Bounds and Finiteness of Graphs from Local Intersection Data): For every integer m ≥ 2, the m-fold Cartesian power of the icosahedron graph is an amply regular graph with parameters (v, k, λ, μ) = (12^m, 5m, 2, 2) and diameter 3m, satisfying μ > 1 and diam(G) > 2k/(λ+2), while having order strictly greater than 12.

Open. seidel_matrix_book_ramsey_lower_bound (arXiv:2610.36522 Corollary 8): Let n ≥ 2 be an integer, and let G be a simple graph on a finite vertex set V of cardinality 4n - 2 with Seidel matrix S. If every row sum of S is 1 and (S^2)_{ij} ≤ 0 for all distinct vertices i ≠ j, then every pair of adjacent vertices in G has at most n -…

The Proposer read 0 new paper(s) and listed 0 open problem(s); 17 new question(s) of AFTD's own were adopted onto the list; 13 list entries were stated in Lean, as were 10 results the papers prove; the Proposer posed 48 more from what the knowledgebase already holds (168 new theorem statement(s) in all, each checked against its English in both directions). The Prover proved 194 theorem(s), 142 of them helper lemmas, which are not listed below; 31 of today's statements are not yet proved and stay in the knowledgebase, marked as such.

Partial result on OP-613. gen_k_server_uniform_log_competitive (arXiv:2610.37192): For every k ≥ 1, every m and every start configuration a : Fin k → Fin m of generalized k-server on k uniform metrics with m points each (unit distances), there are transition probabilities P with gen_k_server_uniform_is_rand_alg P such that for every finite…

Partial result on OP-613. gen_k_server_uniform_one_server_competitive_one (arXiv:2610.37192): With one server (k = 1, configurations Fin 1 → Fin m) and any start configuration a, there are transition probabilities P with gen_k_server_uniform_is_rand_alg P whose expected cost on every request list ρ is at most gen_k_server_uniform_opt a ρ.

Partial result on OP-205. cycle_power_sixteen_block_vertical_average_barrier (arXiv:2610.15635): Eight tight radius16 dyadic profiles with positive integer weights totaling60 satisfy optimal mean size5, all exact dyadic pair averages, every ordinary pair-coverage average, and monotone outer eighths; the weighted upper-vertical defect at offsets1/3…

Partial result on OP-205. cycle_power_exact_rank_boundary_successor (arXiv:2610.15635): For an exact dyadic-rank matching with both parent implications, if a root selects the last lower offset2q-1 and the edge one unit longer than that rank is covered, its owner has offset a<q and root at least p+q. Unless a=q-1, it also owns the next…

Partial result on OP-205. cycle_power_rooted_reflect_exact (arXiv:2610.15635): Reflection of rooted profiles preserves exact pair ownership at every rank length L with0<L<=D; the physical starting point changes from v to -v-(D-L).

Partial result on OP-205. cycle_power_rooted_reflect_cover (arXiv:2610.15635): Reflection preserves coverage of every ordinary distance strictly between0 and the arc length.

Partial result on OP-205. cycle_power_rooted_reflect_parent (arXiv:2610.15635): Reflection preserves both parent implications at every even rank2q, interchanging the lower and upper branches.

Partial result on OP-205. cycle_power_sixteen_block_geometry_reflect (arXiv:2610.15635): The full radius16h Geometry hypotheses, including all ordinary distances and exact12h/14h/15h ownership, are preserved by simultaneous root and offset reflection.

Thread RT-1. cycle_power_fifteen_tight_type_sequence_eight_iff_nine_core_a01111001: One branch of the window refutation behind cycle_power_fifteen_tight_type_sequence_eight_iff_nine_core: under the layer-free tight-cover constraints for k = 15 and 7 fixed bits of the class-type sequence near position 0, the constraints are contradictory.…

Thread RT-1. cycle_power_fifteen_tight_type_sequence_one_alternates_core_alt00000100: One branch of the window refutation behind cycle_power_fifteen_tight_type_sequence_one_alternates_core: under the layer-free tight-cover constraints for k = 15 and 95 fixed bits of the class-type sequence near position 0, the constraints are contradictory.

Thread RT-1. cycle_power_sixteen_block_no_vertical_overlap: For any positive h and Boolean rooted model of radius16h satisfying the explicit Geometry hypotheses (selected endpoints, three parent matchings, exact12h/14h/15h ownership, monotone outer eighths, full ordinary coverage), suppose globally every selected C_t…

Thread RT-1. cycle_power_sixteen_block_child_forces_full_prefix: Under the explicit Geometry hypotheses and the global no-vertical-defect condition C_t implies A_t, every root with any selected C_t has its entire first2h prefix selected.

Thread RT-1. cycle_power_sixteen_block_overlap_reaches_upper_vertical: Under the explicit Geometry hypotheses, every overlap A_t,C_t selected and A_s missing with t<s<2h forces some upper-half vertical defect: at another integer root r some h<=a<2h selects C_a but misses A_a.

Thread RT-1. cycle_power_dyadic_sixteen_block_geometry: Every tight dyadic rooted model of radius2^(k+4), with all-rank exactness, full ordinary coverage and monotone outer eighths, satisfies the explicit sixteen-block Geometry conditions at h=2^k. This is a faithful bridge with no graph-covering conclusion.

Formalized. finite_bmi_algebra_is_idempotent_semigroup_with_left_units (arXiv:2610.37108 Theorem 3.3): Every finite BMI-algebra is an idempotent semigroup with B, M, and I as left units: let $(A, \cdot)$ be a finite magma equipped with elements $B, M, I \in A$ such that $B$ is a $B$-element ($((Bx)y)z = x(yz)$ for all $x, y, z \in A$), $M$ is an $M$-element…

Formalized. edge_cut_transversal_theorem (arXiv:2610.36821 Theorem 5): Let G be a connected simple graph. Let S be a finite set of edges of G of cardinality k that is an edge cut induced by a vertex subset X (meaning there exists X : Set V such that for all e, e ∈ S ↔ e ∈ G.edgeSet ∧ ∃ u ∈ X, ∃ v ∉ X, e = s(u, v)), such that…

Formalized. edge_geodesic_transversal_bound_of_edge_cut (arXiv:2610.36821 Lemma 3): Let G be a connected simple graph. Let S be a finite set of edges of G that is an edge cut induced by a vertex subset X (meaning there exists X : Set V such that for all e, e ∈ S ↔ e ∈ G.edgeSet ∧ ∃ u ∈ X, ∃ v ∉ X, e = s(u, v)). If for all vertices u, v and…

Formalized. intersecting_uniform_hypergraph_card_le_pow (arXiv:2610.37315 Theorem 1.1 -- The maximum size of intersecting k-graphs with covering number k): Let α be a type with decidable equality and let k ≥ 1 be a natural number. Let ℱ be a finite family of finite subsets of α such that every F ∈ ℱ has cardinality k. Suppose that for all F1, F2 ∈ ℱ, the intersection F1 ∩ F2 is nonempty, and that for every…

Formalized. is_maximal_zero_sum_free_subsequence_sums_pred_eq_univ (arXiv:2610.35819 Section 8): Let G be a finite additive commutative group with decidable equality, let n ≥ 1 be a natural number, and let S be a multiset over G satisfying is_maximal_zero_sum_free n S. Then the finite set of (n - 1)-term subsequence sums of S, subsequence_sums (n - 1)…

Formalized. subsequence_sums_maximal_zero_sum_free_term_mul_pred_eq (arXiv:2610.35819 Proposition 8.2): Let G be a finite additive commutative group with decidable equality and exponent n (AddMonoid.exponent G = n). Let S be a multiset over G satisfying is_maximal_zero_sum_free n S. If some element t of G has multiplicity n - 1 in S (S.count t = n - 1), then…

Formalized. regular_graph_lap_mul_pow_scalar_sub_all_ones_trace (arXiv:2610.36127 Lemma 34): For each d-regular graph G on n vertices and each pair of positive integers i and j, the trace of L(G)^i ((d+1)I_n - J_n)^j equals (d+1)^j ℓ_i(G), where J_n is the all-ones matrix and ℓ_i(G) is the Laplacian trace sequence.

Corrected. not_edge_geodesic_transversal_bound_of_edge_disjoint: The statement edge_geodesic_transversal_bound_of_edge_disjoint is false: The statement is false as formalized because it omits a finiteness hypothesis on G (the paper's Lemma 4 is about finite graphs; edge_geodesic_transversal_number is an infimum over…

Corrected. not_div_padicValNat_dvd_div_padicValNat: The statement div_padicValNat_dvd_div_padicValNat is false: The statement is false for non-prime p. Take d = 6, n = 48, p = 4. Then 0 < 6 and 6 ∣ 48. Since 4 ∤ 6, padicValNat 4 6 = 0, so d / 4^{padicValNat 4 6} = 6. Since 4^2 = 16 divides 48 but 4^3 = 64…

Open. uniform_kserver_randomized_competitive (arXiv:2610.37192 Theorem 1.1 -- Tight Bounds for Randomized Generalized k-Server on Uniform Metrics): Let k be a positive integer, let M be a family of uniform metric spaces indexed by Fin k with decidable equality, and let a be an initial configuration. For every finite request sequence ρ, the expected cost uniform_kserver_expected_cost k a ρ of the…

Open. amply_regular_diameter_bound_conjecture (arXiv:2610.36620): Conjecture 3.7 of arXiv:2610.36620: every amply regular graph G on a finite vertex set with parameters (k, ℓ, μ) and μ > 2 has diameter at most 2 * k / (ℓ + 2).

Open. amply_regular_diameter_bound_qpk (arXiv:2610.36620): Theorem 1.3 of arXiv:2610.36620: every amply regular graph G on a finite vertex set with parameters (k, ℓ, μ) satisfying μ > 1 and μ ≥ ℓ has diameter at most 2 * k / μ + 1.

Open. binary_nonzero_common_difference_octuple_count: In any finite commutative exponent-two group with at least8 elements, the number of injective nonzero ordered8-tuples satisfying the stated zero-sum/common-nonzero-difference constraint equals the stated product of group-cardinality factors.

Open. digraph_five_strong_semicomplete_multipartite_two_linked (arXiv:2610.36895): Problem 5.2 (OP-621): Every 5-strong semicomplete multipartite digraph is 2-linked.

Open. digraph_five_strong_co_bipartite_unilaterally_two_linked (arXiv:2610.36895): Every 5-strong co-bipartite digraph is unilaterally 2-linked.

The Proposer read 20 new paper(s) and listed 31 open problem(s); 23 new question(s) of AFTD's own were adopted onto the list; 16 list entries were stated in Lean, as were 9 results the papers prove; the Proposer posed 38 more from what the knowledgebase already holds (130 new theorem statement(s) in all, each checked against its English in both directions). The Prover proved 233 theorem(s), 58 of them helper lemmas, which are not listed below; 38 of today's statements are not yet proved and stay in the knowledgebase, marked as such.

Research-level. latin_double_three_tail_count_formula: The open formula in arXiv:2610.29291 Conjecture 6.3: the number of Latin tableaux of shape (k,k-1,...,4,3,3) is 9 times 4 to the power k-3 for every k at least 5. — (medium tier) settles OP-512 (Exact enumeration of Latin tableaux with a double-three staircase tail)

Research-level. wild_number_complete_graph_large_eq (arXiv:2610.22142): For every integer n>=30000001, every natural number k equal to the chromatic number of the line graph of K_n, and every proper edge coloring c of K_n with color set Fin k, the wild number of c equals floor(4*ceil(n/2)/3). Thus the minimum-proper-coloring… — (medium tier) Proves the conjectured equality for every n>=30000001 and every minimum proper edge coloring, establishing sharpness at all sufficiently large orders rather than only the paper's n<=12 range, the isolated n=279 case, or one congruence class

Research-level. maxcut_op89_optimal_strong_equilibrium_negation (arXiv:2610.04948): It is not true that for every finite type V, simple graph G on V with decidable adjacency, and k ≥ 3, the unweighted Max-k-Cut game on G has an optimal coloring that is a strong equilibrium (the negation of maxcut_op89_optimal_strong_equilibrium_exists); the… — (medium tier) Answers the paper's Question 2 negatively for k = 3: a 182-vertex graph (the paper's 91-vertex G_3 with every vertex doubled into independent twins, plus pin edges from each core twin to two anchors) has an optimal Max-3-Cut coloring that is unique up to color permutation and not a strong equilibrium, so no optimal coloring is a strong equilibrium. The paper only shows that some optimal coloring can fail

Partial result on OP-539. third_principal_specialization_card_eq (knowledgebase): The third principal specialization of any finite tree on at least one vertex uniquely determines its number of vertices.

Partial result on OP-545. tournament_near_regular_card_degrees (knowledgebase): In any near-regular tournament on 2m vertices with m ≥ 1, exactly m vertices have out-degree m - 1 and exactly m vertices have out-degree m.

Partial result on OP-517. op_517_zero_excess_of_eq_pair (arXiv:2610.03808): For any instance inst of WiringDiagramPair, if the two signotopes inst.u and inst.v are equal, then inst has braid-move excess 0 (wiring_diagram_zero_excess inst): the distance is 0 and the number of differing triples is 0.

Partial result on OP-517. op_517_zero_excess_of_le_two (arXiv:2610.03808): For any instance inst of WiringDiagramPair on m pseudolines with m ≤ 2, there are no ordered triples in Fin m, so inst.u = inst.v holds vacuously and therefore inst has braid-move excess 0 (wiring_diagram_zero_excess inst).

Partial result on OP-593. cycle_three_proportionally_three_choosable (knowledgebase): The triangle cycle C_3 is proportionally 3-choosable: for every finite color palette α and every assignment L of 3 colors to each vertex, there exists a proper coloring f of C_3 with f(v) ∈ L(v) for all v such that for every color c : α, the number of…

Partial result on OP-595. strong_odd_five_coloring_of_list_colorable (knowledgebase): If a finite simple graph is strongly odd 5-list-colorable, then it admits an ordinary strong odd 5-coloring.

Partial result on OP-596. maxcut_optimal_no_clique_deviation (knowledgebase): In the unweighted Max-k-Cut game on a finite simple graph, no coalition that induces a clique has a strong deviation from a welfare-optimal coloring.

Partial result on OP-596. chordal_maxcut_optimal_strong_equilibrium_of_card_le (knowledgebase): For every finite simple chordal graph G on at most 2k + 1 vertices and every integer k ≥ 3, the unweighted Max-k-Cut game admits an optimal coloring that is a strong equilibrium.

Thread RT-1. simple_graph_cycle_power_dyadic_cover_class_model: Every optimal dyadic cycle-power equivalence cover admits a faithful periodic integer class model with the original rooted classes and real layer colours, tight class weights, constant active counts, exact dyadic coverage, all ordinary coverage, and disjoint…

Thread RT-1. simple_graph_cycle_power_dyadic_cover_fibre_endpoint_unique: In any clique labeling of the cycle power C_n^{2^m-1} with n ≥ 3(2^m-1)+1, each clique contains at most one pair at distance 2^m-1.

Thread RT-1. simple_graph_cycle_power_dyadic_cover_layer_root_unique: In an optimal (m+1)-layer cover of C_n^{2^m-1}, for each layer s and each vertex v, there is a unique offset a ≤ 2^m-1 such that v-a is the root spanning the class of v in layer s.

Thread RT-1. simple_graph_cycle_power_dyadic_cover_edge_span: If a monochromatic clique contains v and v+d with 1 ≤ d < 2^m, its root v-a (with a ≤ 2^m-1) satisfies a < 2^m - d, so the entire edge {v, v+d} is contained in the span of v-a.

Thread RT-1. cycle_power_dyadic_class_weight_eq_of_sum_eq: If the total sum of dyadic class weights over all residues equals the total sum of active counts, then pointwise equality holds for every residue.

Thread RT-1. simple_graph_cycle_power_dyadic_class_model_disjoint_colours: Two active rooted classes at a common vertex with distinct offsets have distinct layer colours.

Formalized. counterexample_partition_diameter_ratio_three_101 (arXiv:2610.28828 -- A counterexample to Gale's conjecture in $\mathbb{R}^3$, Theorem 2): There exists a finite subset V of 3-dimensional Euclidean space of cardinality 101 and strictly positive diameter such that for every 4-partition of V (given by a map c : V → Fin 4), at least one part has diameter strictly greater than 0.88928 times the…

Formalized. six_circle_two_symbols_labeled_impossible (arXiv:2610.33032, Theorem 8): In the anonymous-slip puzzle for six sages seated in a circle with six labeled seats, there is no deterministic protocol c : (Fin 6 × Fin 6 × Fin 6 × Fin 6) → Fin 2 using two symbols {0, 1} such that every sage can reconstruct the full seating permutation…

Formalized. kst_code_density_odd_odd (arXiv:2610.35136, Sharp Bounds for Graph-Codes Avoiding Complete Bipartite Differences, Proposition 3.2): Let s and t be odd natural numbers, and let n be a natural number such that s + t ≤ n. Then the maximum density of a K_{s,t}-code in simple graphs on vertex set [n], kst_code_max_density s t n, is equal to 1/2.

Formalized. partition_family_A_57_evaluation (arXiv:2610.01747 Proposition 6.1): Evaluating the partition cardinality formula with the partition numbers p(54)=386155, p(53)=329931, p(52)=281589, p(51)=239943, p(50)=204226, p(49)=173525, and p(48)=147273 gives 527254, which strictly exceeds 526823 = p(56).

Formalized. unrestricted_partition_family_four_intersecting_and_card (arXiv:2610.01747 Proposition 6.1): For every natural number n ≥ 1, the family partition_A n of partitions of n is 1-intersecting (is_t_intersecting_partition_family 1 (partition_A n)), and its cardinality coerced to ℤ satisfies ((partition_A n).card : ℤ) = partition_number (n - 3 : ℤ) +…

Formalized. difference_squares_avoiding_gp3_bounds (arXiv:2610.34758 Lemma 3.1): Let $p \ge 7$ be a prime and let $A \subset \mathbb{F}_p$ be nonempty. If the set of squared differences $(A - A)^2$ contains no nondegenerate three-term geometric progression, then $|A|^3 \le p^2$, $|A - A| \ge |A|^{5/4}$, and for every $t \in…

Formalized. bmi_is_left_unit_b (arXiv:2610.37108 Proposition 3.1 -- Finite BM-algebras and fixed-point combinators): Let $(A, \cdot)$ be a finite magma equipped with a $B$-element $B$ and an $I$-element $I$. Then $B$ is a left unit: $Bx = x$ for all $x \in A$.

Formalized. bmi_assoc_of_is_b_of_left_unit (arXiv:2610.37108 Proposition 3.1 -- Finite BM-algebras and fixed-point combinators): Let $(A, \cdot)$ be a magma with a $B$-element $B$. If $B$ is a left unit ($Bx = x$ for all $x$), then the operation is associative: $(xy)z = x(yz)$ for all $x, y, z \in A$.

Proved. maxcut_op89_residual_exists_negation: The residual case maxcut_op89_residual_exists of OP-89 is false: it is not true that every finite simple graph G with k ≥ 3, at least 2k+2 vertices, not k-colorable and with a vertex of degree at least 2k, has an optimal Max-k-Cut coloring that is a strong…

Open. cycle_proportional_choice_number_eq_three (knowledgebase): For every integer n ≥ 3, the simple n-cycle C_n is proportionally 3-choosable: for every finite color palette α and every assignment L of 3 colors to each vertex, there exists a proper coloring f of C_n with f(v) ∈ L(v) for all v such that for every color c…

Open. cycle_not_proportionally_two_choosable (knowledgebase): For every integer n ≥ 3, the simple n-cycle C_n is not proportionally 2-choosable: it is not the case that for every finite color palette α and every assignment L of 2 colors to each vertex, there exists a proper coloring f of C_n with f(v) ∈ L(v) for all v…

Open. unicyclic_spectral_sustainability_maximum_degree (knowledgebase): For every integer n >= 9, the maximum degree among spectrally sustainable connected unicyclic simple graphs of order n is equal to ceil(n/2), represented as (n + 1) / 2: every such graph satisfies Delta(G) <= ceil(n/2) and the bound is attained.

Open. sparse_strong_odd_five_list_coloring (knowledgebase): Every finite simple graph G with maximum average degree strictly less than 7/3 (that is, satisfying has_mad_lt G (7 / 3)) is strongly odd 5-list-colorable.

Open. chordal_maxcut_optimal_strong_equilibrium_exists (knowledgebase): For every finite simple chordal graph G and every integer k ≥ 3, the unweighted Max-k-Cut game on G admits an optimal coloring that is a strong equilibrium.

Open. even_odd_cycle_strong_product_equivalence_cover_eq_five (knowledgebase): For every even integer m ≥ 6 and odd integer n ≥ 5, the equivalence covering number of the strong product of cycles C_m and C_n (the strong product of simple_graph_cycle_power m 1 and simple_graph_cycle_power n 1) is equal to 5.

The Proposer read 22 new paper(s) and listed 28 open problem(s); 28 new question(s) of AFTD's own were adopted onto the list; 17 list entries were stated in Lean, as were 9 results the papers prove; the Proposer posed 39 more from what the knowledgebase already holds (281 new theorem statement(s) in all, each checked against its English in both directions). The Prover proved 296 theorem(s), 119 of them helper lemmas, which are not listed below; 77 of today's statements are not yet proved and stay in the knowledgebase, marked as such.

Research-level. postage_stamp_number_neg_two_of_odd_of_mod_sixty_ne: Exact value of the negative-allowed three-stamp number for odd h ≥ 5 with h ≢ 59 (mod 60): n_h(2) - n♭_h(2) = 1 if h ≡ 9 (mod 12), 2 if h ≡ 1, 3, 5, 7 (mod 12), and 3 if h ≡ 11 (mod 12); here n_h(2) = ⌊(h²+6h+1)/4⌋. — (medium tier) Determines n♭_h(2) exactly for all odd h ≥ 5 except h ≡ 59 (mod 60), where arXiv:2610.19470 only shows n♭_h(2) < n_h(2): the gap n_h(2) - n♭_h(2) is 1 iff h ≡ 9 (mod 12), 2 for h ≡ 1, 3, 5, 7 (mod 12) and 3 for h ≡ 11 (mod 12); for h ≡ 59 (mod 60) it is at least 4, and it is at least 6 at h = 419

Research-level. postage_stamp_number_neg_two_add_four_le_of_mod_sixty_eq: For odd h ≥ 5 with h ≡ 59 (mod 60), n♭_h(2) ≤ n_h(2) - 4, where n_h(2) = ⌊(h²+6h+1)/4⌋. — (medium tier) a new question answered: For h ≡ 59 (mod 60) the gap is at least 4: at range n_h(2) - 3 the Theorem 4.1 inequalities leave only sets with gcd(x, y) > 1 or a divisibility contradiction.

Research-level. mondrian_no_perfect_three_prime_area_one_factor (arXiv:2610.19193): For three distinct primes p,q,r with p>r+1, no perfect admissible integer square partition has common tile area q^s*r*p^a, for arbitrary natural a and s. — (low tier) Excludes perfect partitions of every integer square with common tile area q^s*r*p^a for distinct primes p,q,r with p>r+1, uniformly in a and s. This extends the two-prime common-area obstruction by using the superincreasing signed-height argument

Partial result on OP-529. exists_non_circulant_sharp_cyclic_graph_order_eight (arXiv:2610.31807): There exists a simple graph G on ZMod 8 with at least one edge that admits a sharp cyclic labeling and is not a circulant graph on ZMod 8.

Partial result on OP-529. circulant_graph_admits_sharp_cyclic_labeling (arXiv:2610.31807): For every N ≥ 1 and every subset s of ZMod N, if the circulant graph SimpleGraph.circulantGraph s has at least one edge, then it admits a sharp cyclic labeling on ZMod N.

Partial result on OP-529. sharp_cyclic_graph_is_regular (arXiv:2610.31807): Every finite simple graph G with at least one edge that admits a sharp cyclic labeling on ZMod N is regular of some degree d.

Partial result on OP-518. op_518_positive_fibre_adj_of_adj (arXiv:2610.03808): For every natural number m > 0, and any functions u, v : OrderedTriple (Fin m) → ℤˣ that are rank-3 signotopes whose positive fibres are uniform rank-3 chirotopes on WithTop (Fin m), if u and v are adjacent in the higher Bruhat order bruhat_order_three_graph…

Partial result on OP-517. op_517_zero_excess_iff_exists_walk (arXiv:2610.03808): Two rank-3 signotopes on Fin m have braid-move excess 0 if and only if there exists a walk in the higher Bruhat order B(m, 2) between them whose length equals their Hamming distance.

Partial result on OP-517. op_517_zero_excess_of_eq (arXiv:2610.03808): Every rank-3 signotope on Fin m has braid-move excess 0 with respect to itself: the distance in B(m, 2) from u to u is 0, which equals the number of triples on which u differs from u.

Partial result on OP-163. hunger_transient_time_eq_zero_of_mem_basin (arXiv:2610.08949): For a natural number n with [NeZero n], a rational matrix P : Matrix (Fin n) (Fin n) ℚ, a natural number T, and a rational vector h : Fin n → ℚ, if h belongs to hunger_recurrent_basin P T, then hunger_transient_time P T h = 0.

Partial result on OP-163. hunger_transient_polynomial_bound_of_mem_basin (arXiv:2610.08949): For a natural number n with [NeZero n], a rational matrix P : Matrix (Fin n) (Fin n) ℚ, a natural number T, and a rational vector h : Fin n → ℚ, if h belongs to hunger_recurrent_basin P T, then (hunger_transient_time P T h : ℚ) ≤ (1 : ℚ) * ((n : ℚ) + (T : ℚ)…

Thread RT-1. cycle_power_fifteen_tight_type_sequence_one_iff_fourteen: In the layer-free tight-class model for bandwidth fifteen, the first inner position belongs to a class exactly when the penultimate position does.

Thread RT-1. cycle_power_fifteen_tight_type_sequence_two_iff_three_core_b0: One branch of the window refutation behind cycle_power_fifteen_tight_type_sequence_two_iff_three_core: under the layer-free tight-cover constraints for k = 15 and 8 fixed bits of the class-type sequence near position 0 (a branch of the case split), the…

Thread RT-1. cycle_power_fifteen_tight_type_sequence_two_iff_three_core_b1: One branch of the window refutation behind cycle_power_fifteen_tight_type_sequence_two_iff_three_core: under the layer-free tight-cover constraints for k = 15 and 26 fixed bits of the class-type sequence near position 0 (a branch of the case split), the…

Thread RT-1. cycle_power_fifteen_tight_type_sequence_two_iff_three_core_a0000: One branch of the window refutation behind cycle_power_fifteen_tight_type_sequence_two_iff_three_core: under the layer-free tight-cover constraints for k = 15 and 13 fixed bits of the class-type sequence near position 0 (a branch of the case split), the…

Thread RT-1. cycle_power_fifteen_tight_type_sequence_two_iff_three_core_a0001000: One branch of the window refutation behind cycle_power_fifteen_tight_type_sequence_two_iff_three_core: under the layer-free tight-cover constraints for k = 15 and 79 fixed bits of the class-type sequence near position 0 (a branch of the case split), the…

Thread RT-1. cycle_power_fifteen_tight_type_sequence_two_iff_three_core_a0001001: One branch of the window refutation behind cycle_power_fifteen_tight_type_sequence_two_iff_three_core: under the layer-free tight-cover constraints for k = 15 and 16 fixed bits of the class-type sequence near position 0 (a branch of the case split), the…

Formalized. hamming_equilateral_triangle_local_types (arXiv:2610.32789 "Triangle-Free Sets in Exact-Distance Hamming Graphs", Proposition 2.2): Suppose $x, y, z : \mathrm{Fin}\, n \to \alpha$ satisfy $\mathrm{hammingDist}(x, y) = r$, $\mathrm{hammingDist}(x, z) = r$, and $\mathrm{hammingDist}(y, z) = r$. If $a_x, a_y, a_z$ count the coordinates where $x, y, z$ respectively are exceptional and $d$…

Formalized. unit_hamming_max_triangle_free_eq (arXiv:2610.32789 Theorem 1.3): For every fixed integer q ≥ 2 and every integer n ≥ 1, the maximum size unit_hamming_max_triangle_free n q of a triangle-free vertex subset of (Fin n → Fin q) in the unit-distance Hamming graph equals 2 * q ^ (n - 1).

Formalized. frobenius_extremal_family_frobenius_number (scout/2610-32219-a-sharp-upper-bound-for-the-frobenius-number.md:450): For any integers n ≥ 3 and q ≥ 2, the Frobenius number of the extremal family frobenius_extremal_family n q is equal to ((n - 2) * q + 1) * q - (n - 1) * q - 1.

Formalized. simple_graph_t_chromatic_ps_determines_chromatic_ps (arXiv:2610.31785, Proposition 3.9): Let G and H be finite simple graphs on finite vertex types V and W, respectively, and let n be a positive integer. If the n-th principal specialization of the t-chromatic symmetric function of G equals that of H, then the n-th principal specialization of the…

Formalized. card_two_stack_sortable_perm_ending_in_zero (arXiv:2610.32824 Theorem 1.3): For every non-negative integer n, the number of permutations of {0, 1, ..., n} that end with 0 and are 2-stack-sortable is equal to the n-th Motzkin number.

Formalized. simple_graph_t_chromatic_ps_vertex_count_eq (arXiv:2610.31785 (Principal specializations of the t-chromatic symmetric function), Proposition 3.16(1)): Let n ≥ 2 and let G be a finite simple graph with at least 2 vertices that has a proper coloring with n colors (χ_G(n) > 0). Let d and D be the minimum and maximum degrees of q appearing in the n-th principal specialization ps_n(Z_G(x; t)) (the least and…

Formalized. simple_graph_t_chromatic_ps_q_coeff_symm (arXiv:2610.31785 (Principal specializations of the t-chromatic symmetric function), Proposition 3.16(2)): Let n ≥ 2 and let G be a finite simple graph with at least 2 vertices that has a proper coloring with n colors. Let d and D be the minimum and maximum degrees of q appearing in ps_n(Z_G(x; t)). Then for every j with d ≤ j ≤ D, the coefficient of q^j in…

Formalized. simple_graph_t_chromatic_ps_coeff_t_two_connected_bipartite (arXiv:2610.31785 (Principal specializations of the t-chromatic symmetric function), Proposition 3.16(3); the bipartition is given as a…): Let n ≥ 2 and let G be a connected finite simple graph with at least 2 vertices that has a proper coloring with n colors, and let b : V → Fin 2 be a proper 2-coloring of G (so G is bipartite). Let c1 and c2 be the smaller and the larger of the sizes of the…

Corrected. not_p7_claw_free_dominating_pair_of_no_hole: The statement p7_claw_free_dominating_pair_of_no_hole is false: The statement is FALSE. A concrete counterexample is the net graph (a central triangle with a pendant vertex attached to each vertex of the triangle) on 6 vertices: - Vertex set: {0, 1, 2, 3,…

Corrected. not_rank_score_veto_core_side_count_bound: The statement rank_score_veto_core_side_count_bound is false: The conclusion has its two cardinalities swapped with respect to the paper's lemma (and with respect to the informal statement). In Lean, candidate_rank ord c = #{c' : c < c'} (verified: rank…

Open. op_518_positive_fibre_isometry (arXiv:2610.03808): For every natural number m > 0, and any functions u, v : OrderedTriple (Fin m) → ℤˣ that are rank-3 signotopes whose positive fibres are uniform rank-3 chirotopes on WithTop (Fin m), the mutation walk distance between their positive fibres in…

Open. simple_graph_cycle_power_dyadic_cover_class_model: Every optimal dyadic cycle-power equivalence cover admits a faithful periodic integer class model with the original rooted classes and real layer colours, tight class weights, constant active counts, exact dyadic coverage, all ordinary coverage, and disjoint…

Open. cyclic_matrix_fourier_antidiagonal_iff_circulant: A complex matrix M indexed by ZMod N has its two-dimensional cyclic Fourier transform supported on the anti-diagonal m + n = 0 if and only if M is a circulant matrix.

Open. sharp_cyclic_and_compl_iff_circulant (arXiv:2610.31807 Proposition 4.9 -- Additive energy and Fourier complexity of graphs): Let G be a simple graph on ZMod N, and let G^c be its complement graph. Suppose that both G and G^c have at least one edge. The standard cyclic labeling is sharp for both G and G^c if and only if the adjacency matrix of G is circulant.

Open. cycle_power_dyadic_endpoint_overlap: Conjectured uniform endpoint-overlap core: every class other than the ending class that is active at its last vertex intersects the class starting immediately afterward, in a periodic tight dyadic model with constant optimal count and full coverage.

Open. rational_hunger_game_transient_polynomial_bound (arXiv:2610.08949): There exist natural numbers C and d such that for every natural number n with [NeZero n], every rational matrix P : Matrix (Fin n) (Fin n) ℚ in Matrix.rowStochastic ℚ (Fin n) that is irreducible (is_irreducible_matrix P), every stationary distribution π :…

The Proposer read 11 new paper(s) and listed 24 open problem(s); 14 list entries were stated in Lean, as were 12 results the papers prove; the Proposer posed 49 more from what the knowledgebase already holds (200 new theorem statement(s) in all, each checked against its English in both directions). The Prover proved 244 theorem(s), 158 of them helper lemmas, which are not listed below; 35 of today's statements are not yet proved and stay in the knowledgebase, marked as such.

Research-level. latin_double_three_tail_four_extensions: Conjecture: every Latin tableau of shape (k,k-1,...,4,3,3), k at least 5, extends in exactly four ways after adding the next top row of length k+1. — (medium tier) a new question answered: Evaluate every individual availability permanent as 4 on the double-3-tail staircase family, rather than merely expressing the total count as a sum of unknown permanents or proving top-row monotonicity.

Research-level. mondrian_no_perfect_prime_mul_prime_pow (arXiv:2610.19193): For every pair of distinct primes p and q and every natural exponent e, the square of side q times p^e has no perfect admissible integer rectangle partition. — (medium tier) Excludes every square side q*p^e for distinct primes p,q with no bound on e and no ordering restriction on the primes; arXiv:2007.09639 Theorem 4.1 excludes prime powers and products of at most three primes but does not give this exponent-uniform two-prime family

Research-level. mondrian_no_perfect_two_prime_area (arXiv:2610.19193): For any distinct primes p and q and natural exponents s and t, no perfect admissible partition of any integer square can have common tile area q^s*p^t. — (medium tier) Excludes perfect partitions of every integer square when the common tile area is q^s*p^t for distinct primes p,q and arbitrary exponents, and hence excludes all square sides supported on two primes. The prime-power and small prime-product exclusions of arXiv:2007.09639 Theorem 4.1 and the density theorem in HAL:hal-05729522v2 do not give this uniform common-area restriction

Research-level. round_robin_pne_ef1_of_card_le_two_mul_add_one: With n agents and at most 2n + 1 goods, every pure Nash equilibrium of Round-Robin (nonnegative additive valuations) is EF1. For three agents this is tight: arXiv:2610.23686 Proposition 1 has a non-EF1 equilibrium with eight goods. Whether 2n + 2 goods can break EF1 for every n >= 4 is open. — (low tier) Proves exact EF1 for every number of agents when m <= 2n+1, a positive guarantee beyond the general 1/2-EF1 bound and the three-agent/eight-good counterexample in arXiv:2610.23686

Research-level. simple_graph_hop_or_leap_maximal_not_matroid_flats (arXiv:2610.18463): Neither the collection of hop-closed edge subsets nor the collection of leap-closed edge subsets forms the set of flats of a matroid for every finite simple graph G. — (low tier) refutes OP-302 (Matroid flats from hop-maximal and leap-maximal subgraphs)

Research-level. wild_number_complete_graph_279_min_proper_coloring_eq (arXiv:2610.22142): New case of OP-306: every minimum proper edge colouring of K_279 has wild number 186 = floor(4*ceil(279/2)/3). The lower bound is the paper's; the matching upper bound comes from a seal-free partition of the vertices into 93 triples, found with a local lemma… — (low tier) Proves the conjectured value of the wild number, floor(4*ceil(n/2)/3) = 186, for every minimum proper edge colouring of K_279, a case far beyond the range 3 <= n <= 12 where the paper verified it; the upper bound comes from a seal-free triple partition obtained with a local lemma for random permutations and an exact rational certificate

Partial result on OP-86. maxcut_optimal_not_strong_degree_66 (arXiv:2610.04948): There is a finite simple graph of maximum degree at most 66 with an optimal coloring of the Max-3-Cut game that is not a strong equilibrium; hence Δ*(3) ≤ 65. (The graph G_3 of arXiv:2610.04948, Sec. 2, has 91 vertices and maximum degree 66, attained by the…

Partial result on OP-5. gf8_oracle_min_t_count_ge_20 (arXiv:2610.01024): The slice-rank lower bound: the minimal T-count of the GF(8) multiplication oracle is at least 20.

Partial result on OP-5. gf8_oracle_min_t_count_le_29 (arXiv:2610.01024): The minimal T-count of the GF(8) multiplication oracle is at most 29, certified by an explicit 29-parity representation.

Partial result on OP-314. op314_poset_tower_order_iso_converse (arXiv:2610.20802): For any natural number k and any types α and β equipped with partial orders [PartialOrder α] and [PartialOrder β], if there exists an order-isomorphism α ≃o β, then there exists an order-isomorphism poset_tower α k ≃o poset_tower β k between their height-k…

Partial result on OP-280. mondrian_no_perfect_prime_power (arXiv:2610.19193): No square whose integer side length is a prime power has a perfect admissible partition.

Partial result on OP-305. two_facility_universal_expected_max_cost_nonneg (arXiv:2610.18006): For any universally strategyproof two-facility mechanism M with finite nonempty index type K on a finite nonempty agent set ι in a metric space X and any position profile x : ι → X, two_facility_universal_expected_max_cost M x is nonnegative (0 ≤…

Partial result on OP-280. mondrian_large_prime_descent (arXiv:2610.19193): If c is positive and p is a prime greater than c, any perfect partition of the c times p to the e square yields a perfect partition of the c-square.

Partial result on OP-280. mondrian_perfect_partition_large_prime_iff (arXiv:2610.19193): For every positive integer c, prime p greater than c, and natural exponent e, the square of side c times p to the e has a perfect admissible integer-rectangle partition if and only if the c-square has one.

Thread RT-3. round_robin_pne_envy_zero_ef1_of_two_mul_add_one: With n agents and 2n + 1 goods, in every pure Nash equilibrium of Round-Robin (nonnegative additive valuations) every agent i ≠ 0 is EF1 towards agent 0, the only agent with three goods. With round_robin_pne_ef1_pair_of_count_le_two and…

Thread RT-3. picking_sequence_outcome_pairwise_disjoint: Distinct agents never receive the same good under a picking sequence: the bundles are pairwise disjoint.

Thread RT-3. round_robin_two_mul_add_one_deviation_certificate: Round-Robin with n agents and 2n+1 goods, any reports, agent i ≠ 0: for some good g of agent 0's bundle B_0 (its first pick a1), either some deviation r of agent i alone gets i all of B_0 ∖ {g}, or two deviations r1, r2 of agent i give bundles D1, D2 that…

Thread RT-3. round_robin_two_mul_add_one_outcome_structure: Round-Robin with n agents and 2n+1 goods, any reports: there are goods a2, a3 (agent 0's picks at turns n and 2n) and b1, b2 (agent i's two picks) such that agent 0's bundle is {its first-ranked good, a2, a3}, these three are distinct, agent i's bundle is…

Thread RT-3. round_robin_two_mul_add_one_cover_pairs: Round-Robin with n agents and 2n+1 goods, agent i ≠ 0: let a1 be agent 0's top-ranked good, a2 and a3 the goods it picks at turns n and 2n, and let agent i's bundle be {b1, b2}. Then either some report of agent i alone gives it a bundle containing both a2…

Thread RT-3. picking_turn_alloc_subset: One turn never un-allocates a good: the set of goods already allocated before a picking turn is contained in the set of allocated goods after it.

Formalized. perm_offset_avoiding_count_eq_sum_pie (arXiv:2610.23958 Equation (2)): For every natural number n and finite subset S ⊆ ℤ, the integer count (perm_offset_avoiding_count n S : ℤ) of S-avoiding permutations equals the sum over k from 0 to n of (-1 : ℤ) ^ k * ((n - k).factorial : ℤ) * (perm_offset_rook_number n S k : ℤ).

Formalized. positive_binary_identity_bound_of_perm_cover (arXiv:2610.11098 Lemma 3.6 -- An Improved Lower Bound for Separating Words by Permutation Automata): Let k ≥ 1 be an integer, and let C be a finite set of natural numbers covering the element orders of Equiv.Perm (Fin k) (satisfying is_perm_cover k C). Then there exist distinct binary words u, v : List (Fin 2) with equal counts of each letter (u.count 0 =…

Formalized. simple_graph_is_far_colorable_iff (combinatorics/2610-31489-near-optimal-bounds-for-testing-k-colorability.md:152): A finite simple graph G on a type V with decidable equality and decidable adjacency is ε-far from being k-colorable if and only if every vertex coloring c : V → Fin k satisfies ε * (Fintype.card V : ℝ) ^ 2 ≤ ((simple_graph_monochromatic_edges G c).card : ℝ).

Formalized. two_four_code_sync_single_coord (arXiv:2610.30613, Lemma 2.1): Let $\alpha$ be an alphabet with decidable equality and a distinguished element $0$. Let $\mathcal{C} \subseteq (\mathrm{Fin}\, n \to \alpha)$ be a code containing $0$ such that all distinct codewords have Hamming distance in $\{2, 4\}$. If $x \in…

Formalized. matrix_psd_rank_le_rank_of_hadamard_eq (arXiv:2610.04498 Lemma 2.1 -- Rank-sensitive vertex bounds for semidefinite lifts): For finite types m and n, if M is an entrywise nonnegative real matrix (∀ i j, 0 ≤ M i j) and R is a real matrix such that M = Matrix.hadamard R R, then the positive semidefinite rank of M is at most the ordinary rank of R (matrix_psd_rank M ≤ Matrix.rank R).

Formalized. nonclairvoyant_scheduling_offline_opt_superadditive (arXiv:2610.29037 Lemma 4.2 proof step (1)): For any natural number n and job processing vectors a, z : Fin n → ℝ, the offline optimal total completion time satisfies superadditivity: nonclairvoyant_scheduling_offline_opt a + nonclairvoyant_scheduling_offline_opt z ≤…

Formalized. nonclairvoyant_scheduling_round_robin_hybrid_competitive_ratio (arXiv:2610.29037 Lemma 4.2): Let n be a natural number and let x, a, z : Fin n → ℝ with x = a + z, where a and z have non-negative coordinates (∀ i, 0 ≤ a i and ∀ i, 0 ≤ z i). Suppose an algorithm accumulates non-negative cost C_T ≥ 0 by time T and incurs total completion cost alg_cost…

Formalized. is_k_connected_set_empty (arXiv:2610.29979, Section 2): In every matroid $M$, the empty set is $k$-connected for all $k$.

Corrected. not_is_pk_free_claw_free_hole_dominating: The statement is_pk_free_claw_free_hole_dominating is false: The statement is false as written: it allows k = 4 and m = 3 (since k - 1 = 3 ≤ 3). Counterexample: start from K4 on vertices {0,1,2,3} and attach a pendant vertex 4 adjacent only to 3 (i.e. the…

Corrected. not_single_box_valid_is_partially_adaptive: The statement single_box_valid_is_partially_adaptive is false: The statement is false. IsValidPolicy only constrains the continuation cont v for values v ∈ (inst.dist b).support. In contrast, IsPartiallyAdaptive requires aux order (cont v) for…

Open. op314_poset_tower_two_cancellation (arXiv:2610.20802): For any types α and β equipped with [PartialOrder α], [Fintype α], [Nonempty α], [PartialOrder β], [Fintype β], and [Nonempty β], if there exists an order-isomorphism poset_tower α 2 ≃o poset_tower β 2 between their height-2 exponentiation towers, then there…

Open. op314_cancellation_poset_tower_three (arXiv:2610.20802): For any types α and β equipped with [PartialOrder α], [Fintype α], [Nonempty α], [PartialOrder β], [Fintype β], and [Nonempty β], if there exists an order-isomorphism poset_tower α 3 ≃o poset_tower β 3 between their height-3 right-associated exponentiation…

Open. op314_cancellation_poset_tower (arXiv:2610.20802): For each fixed integer k ≥ 3, and any types α and β equipped with [PartialOrder α], [Fintype α], [Nonempty α], [PartialOrder β], [Fintype β], and [Nonempty β], if there exists an order-isomorphism poset_tower α k ≃o poset_tower β k between their height-k…

Open. two_facility_universal_max_cost_ratio_strictly_below_19_5 (arXiv:2610.18006): In the two-facility location problem with candidate locations on general metric spaces, there exists an approximation ratio α : ℝ with α < 19 / 5 such that for every metric space X : Type*, every candidate set C : Finset X with 2 ≤ C.card, every agent type ι…

Open. op_300_leap_group_prism_and_hypercube (arXiv:2610.18463): Open Problem OP-300: For each odd integer n ≥ 3, the leap group of the prism graph P₁ □ C_n is the full symmetric group on its 2n vertices; for each even integer n ≥ 3, the leap group of P₁ □ C_n has order 2 * (n!)²; and for each integer n ≥ 1, the leap…

Open. two_token_kmn_domination_number (arXiv:2610.28936 Theorem 1.1): Let 2 <= m <= n. The domination number of the 2-token graph F_2(K_{m,n}) is m/2 + n - 1 if m is even; (m-1)/2 + n - 1 if m = 3, or if m is odd, m >= 5, and n = m + 1; and (m-1)/2 + n if m is odd, m >= 5, and n >= m + 2 (or n = m).

Proved. Round-Robin pure Nash equilibria are EF1 for three agents and seven goods

Proved. Line cubic syndrome has a parity representation of 2n plus 1 supports

New result. Unit gap for negative-allowed three-stamp bases occurs exactly when h is 9 modulo 12

Partial. Seventh cycle power requires at least five equivalence subgraphs when eight does not divide n

Lean accepted 1074 new theorems this week, drawn from 90 papers and 23 topics. Of these, 33 are new here, 0 correct a published claim, 154 formalize a published result and 887 are helper lemmas. 6 are research-level results -- they lead the report. 768 statements posed this week are not yet proved. The reading covered 86 new papers. This report covers 9 results in 4 fields.

The Proposer read 0 new paper(s) and listed 0 open problem(s); 18 list entries were stated in Lean, as were 11 results the papers prove; the Proposer posed 37 more from what the knowledgebase already holds (227 new theorem statement(s) in all, each checked against its English in both directions). The Prover proved 205 theorem(s), 155 of them helper lemmas, which are not listed below; 50 of today's statements are not yet proved and stay in the knowledgebase, marked as such.

Research-level. open_problem_line_cubic_t_count (arXiv:2610.01024): For every integer n ≥ 5, there exists a parity representation of the line cubic syndrome of cardinality 2n + 1. — A uniform recursive construction proves that the line cubic has a parity representation of exactly 2n+1 supports for every n≥5, resolving the general case left open beyond the witnesses through n=12 in arXiv:2610.01024

Partial result on OP-446. tetrahedron_boundary_is_partitionable (arXiv:2610.27083): The boundary of a tetrahedron, formed by four triangular facets on four vertices, is partitionable into boolean intervals.

Partial result on OP-437. is_straight_line_cut_consistent_of_parallel_cuts (arXiv:2610.27956): Let P be a finite set of points in ℝ × ℝ, φ a non-zero linear functional from ℝ × ℝ to ℝ, t₁ and t₂ real numbers with t₁ < t₂, and α an allocation function from ℝ × ℝ to Fin 3. If for every point p in P, α p = 0 implies φ p ≤ t₁, α p = 1 implies t₁ ≤ φ p and…

Partial result on OP-437. planar_necklace_two_cuts_six_points (arXiv:2610.27956): For any finite set P of 6 points in the plane ℝ × ℝ colored with two colors c : (ℝ × ℝ) → Fin 2 such that exactly 3 points are colored 0 and 3 points are colored 1, there exists a finite set L of at most 2 straight lines and an allocation function α : (ℝ ×…

Partial result on OP-437. planar_necklace_three_agents_cuts_ge_two (arXiv:2610.27956): Let P be a finite set of points in ℝ × ℝ colored with two colors c : (ℝ × ℝ) → Fin 2, L a finite set of straight lines, and α an allocation function from ℝ × ℝ to Fin 3. If each of the three agents receives exactly 1 point of color 0 and 1 point of color 1…

Partial result on OP-306. wild_number_complete_graph_279_min_proper_coloring_eq (arXiv:2610.22142): New case of OP-306: every minimum proper edge colouring of K_279 has wild number 186 = floor(4*ceil(279/2)/3). The lower bound is the paper's; the matching upper bound comes from a seal-free partition of the vertices into 93 triples, found with a local lemma…

Partial result on OP-1. matrix3_trace_split_reconstruction (arXiv:2610.01639): The cyclic trace coefficient identities reconstruct every 27-coordinate vector through the first-factor column ranges. This is the explicit right-inverse identity behind the split flattening.

Partial result on OP-1. matrix3_trace_rank_sum_ge_27 (arXiv:2610.01639): For a finite family of 3x3 matrices over a field satisfying the cyclic trace identities of matrix multiplication, the sum of the matrix ranks of the first factors is at least 27.

Partial result on OP-396. young_lattice_one_fractional_scd (arXiv:2610.24148): For any positive integer n ≥ 1, the Young lattice L(1, n) admits a fractional symmetric chain decomposition.

Thread RT-1. cycle_power_fifteen_endpoint_layer_period_sixteen: For sixteen-position cyclic class types alternating between endpoint-only types {0,15} and types with equal consecutive membership bits, assume every vertex is active in exactly five classes, the active classes have distinct labels in Fin 5, and every class…

Formalized. canonical_permutation_avoidance_of_local_lemma (Using Lovász Local Lemma in the Space of Random Injections, Electronic Journal of Combinatorics 14 (2007), R63, DOI 10.37236/981, Theorem…): For finitely many injective partial assignments on n points, if weights in [0,1) satisfy the asymmetric local-lemma inequalities for the graph connecting assignments with overlapping domains or ranges, some permutation avoids every assignment.

Formalized. simple_graph_rich_witness_graph_coloring_iff (arXiv:2610.16446, Section 2, Lemma 3 and its direct converse, in the simple-graph specialization.): Colorability of the prescribed-witness graph is equivalent to a proper edge-coloring of G in which every prescribed edge of R is rich.

Formalized. pell_number_closed_form (arXiv:2610.08525 Appendix A): For every natural number m, twice the m-th Pell number equals ((1 + Real.sqrt 2) ^ m - (1 - Real.sqrt 2) ^ m) / Real.sqrt 2.

Formalized. brgc_inverse_flip_preserves_cut_max (Gray-ordered Binary Necklaces (2007), Theorem 3.6, in the equivalent convention of maximal forward Gray rank; the rotation form adds…): If an n-bit word has strictly greater inverse Gray rank than every nontrivial cyclic cut, toggling its last bit has at least as great an inverse Gray rank as every nontrivial cyclic cut of the toggled word.

Formalized. brgc_inverse_flip_preserves_rotation_max (Gray-ordered Binary Necklaces (2007), Theorem 3.6, in the equivalent convention of maximal forward Gray rank; the rotation form adds…): Toggling the last bit of an aperiodic nonconstant word that maximizes its inverse Gray rank over all rotations again maximizes that rank, for word length at least two.

Formalized. matrix_eigenvalues₀_le_of_sub_posSemidef (scout/2610-10618-the-hellinger-conjecture-for-antipodal-boolean-functions.md:402): If $A$ and $C$ are real symmetric matrices such that $C - A$ is positive semidefinite, then each ordered eigenvalue of $A$ is at most the corresponding ordered eigenvalue of $C$.

Formalized. matrix_nuclear_norm_eigenvalue_inequality (arXiv:2610.10618 Lemma 2.2 -- The Hellinger Conjecture for Antipodal Boolean Functions): Let $n$ be a finite type with decidable equality. Let $A$ and $B$ be real symmetric matrices indexed by $n \times n$, with eigenvalues $a_j$ and $b_j$ in nonincreasing order. Then the sum over $j \in \mathrm{Fin}(|n|)$ of $|a_j - b_j|$ is at most the nuclear…

Formalized. matrix_nuclear_norm_of_isHermitian (scout/2610-10618-the-hellinger-conjecture-for-antipodal-boolean-functions.md:315): For a real symmetric matrix $M$, its nuclear norm equals the sum of the absolute values of its eigenvalues.

Open. cohen_macaulay_two_complex_partitionable (arXiv:2610.27083): Every finite pure two-dimensional Cohen-Macaulay simplicial complex over a field k is partitionable into boolean intervals indexed by its facets.

Open. arrows_realization_up_to_63 (arXiv:2610.15145 Theorem 7.3): Every natural number g with g ≤ 63 is realizable as the Grundy value of the Game of Arrows on some finite tree. Furthermore, every finite tree with Grundy value at least 2 has at least 17 vertices, every finite tree with Grundy value at least 4 has at least…

Open. open_problem_young_lattice_fractional_scd (arXiv:2610.24148): For all positive integers m, n ≥ 1, the Young lattice L(m, n) of partitions bounded in an m × n box admits a fractional symmetric chain decomposition with respect to its natural centered rank.

Open. arrows_twin_branch_reduction (arXiv:2610.15145 Theorem 5.6): Let c be a vertex of a tree T, and let B₁, B₂ be distinct components of T - c that are isomorphic via an isomorphism φ from T[B₁ + c] to T[B₂ + c] fixing c. Let T' be obtained from T by deleting B₁ ∪ B₂ and attaching a new pendant edge at c. Then the Grundy…

Open. op_380_thirteen_edge_connected_has_modulo_seven_orientation (arXiv:2610.07034): Every 13-edge-connected finite simple graph has a modulo-7 orientation.

Open. kneser_hom_cycle_reduction_to_cycle_with_chords (arXiv:2610.17884 Lemma 4.1): Let k ≥ 2, m ≥ 6, and 3 ≤ a ≤ m - 3. For every graph G, there exists a graph homomorphism from the G-stable Kneser graph of the disjoint sum of G and the (m-1)-cycle to the G-stable Kneser graph of the disjoint sum of G and the m-cycle with two chords {1, a}…

The Proposer read 0 new paper(s) and listed 1 open problem(s); 14 list entries were stated in Lean, as were 8 results the papers prove; the Proposer posed 49 more from what the knowledgebase already holds (193 new theorem statement(s) in all, each checked against its English in both directions). The Prover proved 203 theorem(s), 145 of them helper lemmas, which are not listed below; 32 of today's statements are not yet proved and stay in the knowledgebase, marked as such.

Research-level. postage_stamp_number_neg_two_add_one_eq_iff: For odd h ≥ 5, the negative-allowed three-stamp number misses n_h(2) = ⌊(h²+6h+1)/4⌋ by exactly one, n♭_h(2) = n_h(2) - 1, if and only if h ≡ 9 (mod 12). — a new question answered: decides when the strict inequality n♭_h(2) < n_h(2) loses only one: exactly when h ≡ 9 (mod 12) (h ≥ 5)

Research-level. postage_stamp_number_neg_four_one_nine_two_add_six_le: For h = 419 (h ≡ 59 mod 60), the negative-allowed three-stamp number satisfies n♭_h(2) ≤ n_h(2) - 6, where n_h(2) = ⌊(h²+6h+1)/4⌋ = 44519. This refutes the conjectured value n♭_h(2) = n_h(2) - 4 for h ≡ 59 (mod 60) (postage_stamp_number_neg_two_of_odd). — a new question answered: At h = 419 the gap is at least 6: the Theorem 4.1 inequalities at range N - 5 leave only six sets a + {0,x,y}, and each has gcd(x,y) > 1 (y = 210 = 2·3·5·7 with x ∈ {3,5,7,9}, or y = 212 with x ∈ {138,140}).

Refutes OP-182. op182_deferred_to_deadline_beyond_half_against_stopping (arXiv:2610.13775): Refutation of Open Problem OP-182 against the deferred-until-stopping benchmark: there does not exist any constant c > 1/2 such that for every Pandora's problem instance with deadlines inst : PandoraDeadlineInstance, there exists a valid adaptive policy…

Partial result on OP-502. prefix_reversal_six_five_three_not_top (arXiv:2610.30892): In the symmetric group Equiv.Perm (Fin 6), the subgroup generated by the three prefix reversals of lengths 3, 5, and 6 does not equal the full symmetric group.

Refutes OP-502. prefix_reversal_necessary_conditions_not_sufficient (arXiv:2610.30892): It is not the case that for all natural numbers 2 ≤ k < m < n satisfying 2 * m > n, at least one of k, m, n even, at least one of k, m, n congruent to 2 or 3 mod 4, gcd(gcd(k, m), n) = 1, m + k ≥ n + 1, and gcd(n - m, n - k) = 1, the three prefix reversals…

Partial result on OP-502. prefix_reversal_gcd_diff_necessary (arXiv:2610.30892): If three prefix reversals of lengths k, m, n with 2 ≤ k < m < n generate the symmetric group Equiv.Perm (Fin n), then gcd(n - m, n - k) = 1.

Answers OP-494. op_494_additive_chromatic_bipartite_maxDegree (arXiv:2610.30174): Let G be a finite connected bipartite simple graph with maximum degree at least 2. Then there exists a vertex labeling f : V → ℕ such that 1 ≤ f(v) ≤ G.maxDegree for all v, and adjacent vertices have different neighborhood sums ∑_{w ∈ N(u)} f(w) ≠ ∑_{w ∈…

Partial result on OP-494. additive_coloring_bipartite_maxDegree_add_one (arXiv:2610.30174): Every finite connected bipartite graph with maximum degree at least 2 admits an additive coloring f with 1 ≤ f(v) ≤ Delta(G) + 1 for all vertices v.

Partial result on OP-487. permutahedron_five_not_psd_factorization_six_of_rank_ge_seven (arXiv:2610.04498): If the positive semidefinite rank of the slack matrix of the standard five-element permutahedron is at least 7, then the slack matrix has no positive semidefinite factorization of size 6.

Partial result on OP-487. permutahedron_five_xc_psd_ge_six (arXiv:2610.04498): The positive semidefinite rank of the slack matrix of the standard five-element permutahedron is at least 6.

Thread RT-1. cycle_power_fifteen_class_weight_certificate: For a subset of the sixteen positions of an arc, the weighted number of pairs at distances 8, 12, 14, 15, with weights 1, 1, 1, 2, is at most its cardinality.

Thread RT-1. cycle_power_fifteen_tight_class_ancestors: Equality in the sixteen-position weighted-pair bound forces equal endpoint bits and closure under the fourteen parent edges of its rooted forest.

Thread RT-1. cycle_power_fifteen_tight_class_spanning: Every nonempty subset attaining equality in the sixteen-position weighted-pair bound contains both positions 0 and 15.

Thread RT-1. cycle_power_fifteen_type_layer_periods_dvd: For sixteen-position classes on a cyclic index set, type period 8 and layer-label period 16 force 16 to divide the cycle length, provided distinct overlapping classes have different labels and some class contains a distance-8 pair. Labels may lie in any type.

Thread RT-1. simple_graph_cycle_power_fifteen_adj_iff: For n at least 46, adjacency in the fifteenth power of the cycle is displacement by a nonzero integer of absolute value at most 15.

Formalized. poset_nonempty_order_iso_of_card_order_hom_eq_of_connected (arXiv:2610.20802 (Two short proofs of the A^A theorem), Lemma 2.4.): Let X and Y be finite posets (possibly empty). If for every finite nonempty connected poset Z the number of order-preserving maps Z → X equals the number of order-preserving maps Z → Y, then X and Y are order-isomorphic. (A poset is connected when its…

Formalized. postage_stamp_number_two_eq (arXiv:2610.19470 (Positivity and negativity for h-bases for n), Theorem 1.1 (classical; cited there).): The classical postage stamp number for three stamps: n_h(2) = ⌊(h² + 6h + 1)/4⌋ for every h ≥ 1.

Formalized. postage_stamp_number_neg_two_eq_of_mod_four_eq_two (arXiv:2610.19470 (Positivity and negativity for h-bases for n), Theorem 3.3 (with the value of n_h(2) from Theorem 1.1).): If h ≥ 2 and h ≡ 2 (mod 4), then n♭_h(2) = n_h(2) = (h² + 6h)/4.

Formalized. mutual_f_information_subadditive_full_support_of_weight_bound (arXiv:2610.21231 (On the subadditivity of mutual f-information), Theorem 1. Differs: the conclusion is for full-support distributions (the…): Theorem 1 of arXiv:2610.21231, on full-support distributions. Let f with f(1) = 0 be convex and four times continuously differentiable on (0, ∞), and g(x) = x² f''(x). If g''(x) < 0 for all x > 0 and there are constants η > 0 and ℓ with g(x) + 2(g'(x) -…

Formalized. subadditive_mutual_f_information_family_full_support (arXiv:2610.21231 (On the subadditivity of mutual f-information), Corollary 1. Differs: subadditivity is stated for full-support…): Corollary 1 of arXiv:2610.21231, on full-support distributions: let s be twice continuously differentiable, positive and concave on (0, ∞) with s'' < 0, let K_s(x) = s(x) + 2(s'(x))²/(-s''(x)) be concave on (0, ∞), and let α ≥ K_s(1). Then f(x) = α x log x +…

Formalized. hash_potential_of_length_eq (arXiv:2610.31363 Lemma 4.2): For any sequence A of length t, the potential hash_potential n r S t A equals the number of slots in S occupied by A, hash_occupy_count n r S A.

Formalized. digraph_semisaturation_bounded_of_isolated_edge (arXiv:2610.18600 Lemma 2.1): Let G : Digraph V be a finite oriented digraph on vertex type V with DecidableEq V and DecidableRel G.Adj such that digraph_is_oriented G and digraph_has_isolated_edge G hold. Then the semisaturation function is bounded: there exist C : ℕ and n₀ : ℕ such…

Formalized. permutahedron_slack_matrix_nonneg (arXiv:2610.04498 Sec. 4.2): For every natural number n, nonempty proper subset S of Fin n, and permutation σ of Fin n, the entry of the permutahedron slack matrix at (S, σ) is nonnegative.

Proved. postage_stamp_number_neg_two_of_odd_of_mod_sixty_ne: Exact value of the negative-allowed three-stamp number for odd h ≥ 5 with h ≢ 59 (mod 60): n_h(2) - n♭_h(2) = 1 if h ≡ 9 (mod 12), 2 if h ≡ 1, 3, 5, 7 (mod 12), and 3 if h ≡ 11 (mod 12); here n_h(2) = ⌊(h²+6h+1)/4⌋.

Proved. postage_stamp_number_neg_two_add_four_le_of_mod_sixty_eq: For odd h ≥ 5 with h ≡ 59 (mod 60), n♭_h(2) ≤ n_h(2) - 4, where n_h(2) = ⌊(h²+6h+1)/4⌋.

Corrected. not_prefix_reversal_sum_bound_necessary: The statement prefix_reversal_sum_bound_necessary is false: The statement claims that m + k ≥ n + 1 is a necessary condition for prefix reversals of lengths k, m, n to generate S_n. However, for (k, m, n) = (2, 3, 5), the prefix reversals of lengths 2, 3,…

Corrected. not_fair_binomial_anticoncentration_bound: The statement fair_binomial_anticoncentration_bound is false: The statement is false for small α. Take n = 2, α = 1/10, and X the identity on the binomial space Bin(2, 1/2). The interval |X - 1| ≤ (1/10)√2 contains the integer 1, whose binomial probability…

Open. picking_prefix_state_alloc_mono: The set of allocated goods is monotone in the number of turns: if s <= t then the goods allocated after s turns are allocated after t turns.

Open. hash_step_delta_sum_fully_occupied_le (arXiv:2610.31363 Lemma 4.4): For any slot subset S and index i : Fin t, the sum of potential changes hash_potential_delta n r S t ((List.ofFn H).take i.val) (H i) over all sequences H in hash_fully_occupied_seqs n r S t is at most (hash_count_fully_occupied n r S t : ℝ) - (n : ℝ) *…

Open. permutahedron_five_xc_psd_ge_seven (arXiv:2610.04498): The positive semidefinite rank of the slack matrix of the standard five-element permutahedron is at least 7.

Open. polygon_psd_rank_four_attains_eight (arXiv:2610.04498): There exists an 8 × 8 real matrix S : Matrix (Fin 8) (Fin 8) ℝ such that is_convex_polygon_slack_matrix 8 S and matrix_has_psd_factorization S 4 hold.

Open. linear_three_graph_le_five_edges_is_iterated_tripartite (arXiv:2610.14829 Proposition 2.8): Every linear 3-uniform hypergraph F with at most 5 hyperedges is iterated tripartite.

Open. cycle_rook_poly_sq_sub (arXiv:2610.23958 Lemma 6.1): For every positive integer n, the square of the rook polynomial of an n-cycle satisfies Q_n(x)^2 = Q_{2n}(x) + 2(-x)^n in ℚ[x].