Mathematical Research

Autonomous conjecture generation and formal verification from axioms. 149 formally proven. 1385 with computational evidence. 178 falsified. 967 lemmas accumulated.

Computational evidence is not presented as proof. Formal proof claims require public Lean4 source in the result manifest.

Ramsey

[1] For any edge 2-coloring of K_47 that avoids monochromatic K_5, the maximum number of monochromatic triangles is at least 4872: Verification: Falsified. Falsified. Report Manifest
[2] In any 2-coloring of the edges of K_35 that contains no red K_4 and no blue K_6, the red subgraph cannot contain a vertex of degree exactly 8. Specifically, the set of red degrees in such an extremal coloring must exclude the integer 8.: Verification: Falsified. Falsified. Report Manifest
[3] In any 2-coloring of the edges of K_43 that contains no monochromatic K_5, there exists no vertex v such that the red degree of v is exactly 22 AND the red neighborhood of v induces a subgraph with fewer than 130 red edges. Equivalently, if a vertex has red…: Verification: Falsified. Falsified. Report Manifest
[4] w(2;4,4) = 35: every 2-coloring of {1,...,35} contains a monochromatic arithmetic progression of length 4. Verify computationally by showing all 2-colorings of {1,...,34} avoid monochromatic AP-4 (proving w > 34), and {1,...,35} does not.: Verification: Falsified. Falsified. Report·DOI Manifest

Number Theory

[5] Conjecture: For the sequence of primes of the form n^2+1, let P_k = n_k^2+1 be the k-th such prime. The difference between consecutive roots, d_k = n_{k+1} - n_k, satisfies d_k <= floor(sqrt(2)*sqrt(n_k)) for all k >= 2. This refines the expected Cramer-type…: Verification: Falsified. Falsified. Report Manifest
[6] For all integers x >= 10,000, the ratio of the actual count of twin prime pairs up to x to the Hardy-Littlewood prediction (2*C2*x/ln(x)^2) is strictly bounded between 0.92 and 1.08. Furthermore, the relative error |actual/predicted - 1| is strictly less…: Verification: Falsified. Falsified. Report Manifest
[7] For any integer N >= 100, let T(N) be the count of twin prime pairs (p, p+2) with p <= N. Let S_3(N) be the count of such pairs where the smaller prime p satisfies p mod 3 == 1. The conjecture states that the deviation of S_3(N) from exactly half of T(N) is…: Verification: Falsified. Falsified. Report Manifest
[8] For any integer n > 1, if n is a perfect power (n = x^a with x > 1, a > 1), then there exists no other perfect power m = y^b (with y > 1, b > 1) in the interval (n, n + n^(2/3)], except for the specific case where n = 8 (2^3) and m = 9 (3^2). This conjecture…: Verification: Falsified. Falsified. Report Manifest
[9] For any integer n >= 2, let P_n be the set of primes of the form k^2+1 where 1 <= k <= n. Let G_n be the maximum gap between consecutive elements in the sorted sequence P_n (defining the first gap as p_1 - 1). Then G_n is strictly less than 2.5 * sqrt(p_max)…: Verification: Falsified. Falsified. Report Manifest
[10] For every Fibonacci prime F_p with index p > 3, the quantity (p-1)/2 is a prime number. In other words, the indices of Fibonacci primes greater than 2 are either 4 or twice a prime (Sophie Germain prime structure in the index).: Verification: Falsified. Falsified. Report Manifest
[11] For every even integer n >= 12, there exists a Goldbach partition n = p + q (with p <= q) such that the smaller prime p satisfies p < sqrt(n) * ln(n) AND p is a quadratic residue modulo the smallest prime factor of n/2. If n/2 is prime, p must be a quadratic…: Verification: Falsified. Falsified. Manifest
[12] For every even integer n >= 14, there exists a Goldbach partition n = p + q (with p <= q) such that the smaller prime p lies in the interval [n/2 - sqrt(n) * ln(ln(n)), n/2]. This conjecture asserts that Goldbach partitions are not only present but can be…: Verification: Falsified. Falsified. Report Manifest
[13] For every even perfect number n > 6, if n is expressed in the Euclidean form n = 2^(p-1) * (2^p - 1) where p is prime, then the sum of the decimal digits of the Mersenne prime factor M_p = 2^p - 1 is strictly greater than the sum of the decimal digits of the…: Verification: Falsified. Falsified. Report Manifest
[14] For every integer n > 1, let S(n) be the set of odd integers encountered in the Collatz trajectory of n before reaching 1 (excluding the final 1). Let M(n) be the maximum element in S(n). If S(n) is non-empty, then M(n) is congruent to 5 modulo 6 if and only…: Verification: Falsified. Falsified. Report Manifest

Graph Theory

[15] In any 2-coloring of the edges of K_18 that achieves the global minimum number of monochromatic K_4 subgraphs, the resulting color classes (graphs) must be isomorphic to each other. Furthermore, each color class must have an automorphism group of order at least 18.: Verification: Falsified. Falsified. Report Manifest
[16] ex(n, K_4) = t_3(n) (Turán number). Verify the Turán graph T(n,3) is the unique extremal graph for K_4-free.: Verification: Computational evidence. Computational evidence; no counterexample in 3,333 cases. Manifest

Formal Identities

[17] For all natural numbers n, the square of a sum of n and 1 is equal to the sum of their squares plus twice their product.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[18] For all natural numbers n, the square of a sum of n and 1 is equal to the sum of their squares plus twice their product.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[19] For any natural number n, the product of n and n+1 is divisible by 2.: Verification: Formal proof verified. Formally proven (Lean4). Report Manifest· Lean4
[20] For any natural number n, the product of n and n+1 is divisible by 2.: Verification: Formal proof verified. Formally proven (Lean4). Report Manifest· Lean4
[21] For any natural number n, the square of n modulo 3 is either 0 or 1.: Verification: Formal proof verified. Formally proven (Lean4). Report Manifest· Lean4
[22] For any natural number n, the square of n modulo 3 is either 0 or 1.: Verification: Formal proof verified. Formally proven (Lean4). Report Manifest· Lean4
[23] For any natural number n, twice the sum of integers from 0 to n equals n times (n+1). Specifically verified for n=100.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[24] For any natural number n, twice the sum of integers from 0 to n equals n times (n+1). Specifically verified for n=100.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[25] For every natural number n, the square of n modulo 4 is either 0 or 1.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[26] For every natural number n, the square of n modulo 4 is either 0 or 1.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[27] For every natural number n, the sum of 2^i for i from 0 to n equals 2^(n+1) - 1.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[28] For every natural number n, the sum of 2^i for i from 0 to n equals 2^(n+1) - 1.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[29] For every non-negative integer n, the product of three consecutive integers n, n+1, and n+2 is divisible by 3.: Verification: Formal proof verified. Formally proven (Lean4). Report Manifest· Lean4
[30] For every non-negative integer n, the product of three consecutive integers n, n+1, and n+2 is divisible by 3.: Verification: Formal proof verified. Formally proven (Lean4). Report Manifest· Lean4
[31] The sum of the first n odd positive integers equals n squared for any natural number n.: Verification: Formal proof verified. Formally proven (Lean4). Report Manifest· Lean4
[32] The sum of the first n odd positive integers equals n squared for any natural number n.: Verification: Formal proof verified. Formally proven (Lean4). Report Manifest· Lean4

Combinatorics

[33] For n ≥ 6, the maximum number of 1s in an n×n 0-1 matrix with no 3×3 all-ones submatrix satisfies z(n,n;3,3) ≤ (n^2 - n)/2 + 1: Verification: Falsified. Falsified. Manifest
[34] For n ≥ 7, the maximum intersecting family of 3-element subsets of {1,...,n} has size C(n-1,2). Verify computationally for all n ≤ 12.: Verification: Computational evidence. Computational evidence; no counterexample in 55 cases. Manifest
[35] For n=6, the maximum size of a cap set in F_3^n is exactly 112. Furthermore, every maximal cap set of this size contains a subset of 28 points that forms a disjoint union of 4 affine planes of dimension 2 (2-flats), where no three of these planes are…: Verification: Falsified. Falsified. Report Manifest
[36] The maximum cap set size in F_3^6 is exactly 112, and this bound is achieved only by the canonical construction S_3^6 ⊂ F_3^6: Verification: Falsified. Falsified. Manifest
[37] [BOUNDED ≤100] z(n,n;2,2) = ⌊(n+1)^2/4⌋: the maximum entries in an n×n 0-1 matrix with no 2×2 all-ones submatrix.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[38] g(7) = 143: every positive integer is the sum of at most 143 seventh powers. Verify g(7) ≤ 143 computationally for small cases.: Verification: Computational evidence. Computational evidence; no counterexample in 1,000 cases. Manifest

Methodology

Each conjecture is generated from the formal statement of an open problem, together with known bounds and previously accumulated results. Before any proof is attempted, a computational search looks for counterexamples. If none is found within the allotted time, a formal proof is attempted using the Lean4 theorem prover with automated error correction. Results of all three kinds are published as independent reports: formal proofs, falsifications, and computational evidence.

Every listed result has a public manifest using the math-result-v1 contract. The manifest separates falsified results, computational evidence, proof attempts, and formally verified proof claims. Lean4 source is linked only when the public manifest can support a formal verification claim.