Mathematical Research

Autonomous conjecture generation and formal verification from axioms. 61 formally proven. 757 with computational evidence. 105 falsified. 578 lemmas accumulated.

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

Ramsey

[1] In any 2-coloring of the edges of K_35 that avoids a red K_4 and a blue K_6 (if such a coloring exists), the maximum degree of any vertex in the red subgraph must be strictly less than 12. That is, Δ(Red) ≤ 11.: Verification: Falsified. Falsified. Manifest
[2] In any 2-coloring of the edges of K_43 that contains no monochromatic K_5, the red subgraph cannot contain a vertex of degree 22 or higher. Specifically, if a valid Ramsey (5,5)-avoiding coloring exists on 43 vertices, the maximum degree of the red subgraph…: Verification: Computational evidence. Computational evidence; no counterexample in 47 cases. 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 21 AND the red neighborhood of v induces a subgraph containing a red triangle. 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] For all integers x >= 100, the absolute difference between the actual count of twin prime pairs up to x and the Hardy-Littlewood prediction (2*C2*x/ln(x)^2) is strictly bounded by the square root of the prediction itself. That is, |pi_2(x) - Li_2(x)| <…: Verification: Falsified. Falsified. Report Manifest
[6] For any even perfect number n > 6, let p be the largest prime factor of n (which is also the Mersenne prime exponent's base, i.e., n = 2^(p-1)*(2^p - 1)). The sum of the proper divisors of the Mersenne prime component (2^p - 1), which is exactly 1, plus the…: Verification: Falsified. Falsified. Report Manifest
[7] For any integer n > 1, if n is a perfect power (n = x^a with x > 1, a > 1), then the distance to the nearest other perfect power m (m != n, m = y^b with y > 1, b > 1) satisfies |n - m| > sqrt(n) * (ln(n))^0.8, with the sole exception of the pair (8, 9) where…: Verification: Falsified. Falsified. Report Manifest
[8] For any integer n > 1, let S(n) be the set of odd integers encountered in the Collatz trajectory of n before reaching 1. Define the 'Odd-Step Parity Signature' P(n) as the sum of the indices (0-based) of all odd elements in S(n) that are congruent to 3…: Verification: Falsified. Falsified. Report Manifest
[9] For every even integer n > 10,000, there exists a Goldbach partition n = p + q (where p and q are primes) such that both p and q are 'isolated' within a window of size W(n) = floor(0.8 * ln(n) * ln(ln(n))). Specifically, there are no other primes in the…: Verification: Falsified. Falsified. Report·DOI Manifest
[10] For every even integer n >= 10,000, there exists a Goldbach partition n = p + q (where p and q are prime) such that both p and q lie within the interval [n/2 - sqrt(n), n/2 + sqrt(n)] AND at least one of the primes p or q has a decimal representation that…: Verification: Falsified. Falsified. Report Manifest
[11] For every index n > 4 such that the Fibonacci number F_n is prime, the index n itself must be a prime number that can be expressed as the sum of two squares (i.e., n is a Pythagorean prime or n=2). Consequently, no Fibonacci prime exists at an index n where…: Verification: Falsified. Falsified. Report Manifest
[12] For every integer N >= 10,000, let T(N) be the count of twin prime pairs (p, p+2) with p <= N. Let S_odd(N) be the sum of the smaller primes p in these pairs where p ends in the digit 3 or 9, and S_even(N) be the sum where p ends in 1 or 7. The conjecture…: Verification: Falsified. Falsified. Report Manifest
[13] For every integer N >= 2, let P_N be the set of primes of the form k^2+1 less than or equal to N. Let M_N be the maximum gap between consecutive elements in the sorted sequence P_N (defining the first gap as p_1 - 0). Then M_N is strictly less than 4 *…: Verification: Falsified. Falsified. Report Manifest
[14] For the sequence of primes of the form p = n^2 + 1, let S(x) be the set of such primes less than or equal to x. Define the 'quadratic gap ratio' for a prime p = n^2 + 1 (where n > 1) as R(p) = (p_next - p) / (2n), where p_next is the next prime in the…: 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

Combinatorics

[17] Conjecture: For n=6, the maximum size of a cap set in F_3^6 is exactly 112, and this maximum is uniquely achieved (up to affine equivalence) by the set of vectors with weight congruent to 1 modulo 3 in the specific coordinate subspace defined by the first 6…: Verification: Falsified. Falsified. Report·DOI Manifest
[18] 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
[19] For n≥3, the maximum number of ones in an n×n matrix avoiding a 3×3 all-ones submatrix is strictly less than n^2, and the difference n^2 - z(n,n;3,3) grows at least linearly with n.: Verification: Falsified. Falsified. Manifest
[20] 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
[21] [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
[22] 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

Formal Identities

[23] For any natural number n, the product of n and (n+1) is divisible by 2.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[24] For any natural number n, the product of n and (n+1) is divisible by 2.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[25] For any 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 any 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 any natural number n, the sum of integers from 0 to n multiplied by 2 equals n times (n+1). Specifically verified for n=100.: Verification: Falsified. Falsified. Report Manifest
[28] For every natural number n less than 100, the expression n squared minus n is even.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[29] For every natural number n less than 100, the expression n squared minus n is even.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[30] For every natural number n, the product of three consecutive integers n, n+1, and n+2 is divisible by 3.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[31] For every natural number n, the product of three consecutive integers n, n+1, and n+2 is divisible by 3.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[32] For every natural number n, the square of n modulo 3 is either 0 or 1.: Verification: Formal proof verified. Formally proven (Lean4). Report Manifest· Lean4
[33] For every natural number n, the square of n modulo 3 is either 0 or 1.: Verification: Formal proof verified. Formally proven (Lean4). Report Manifest· Lean4
[34] For every natural number n, the sum of the first n odd positive integers equals n squared.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[35] For every natural number n, the sum of the first n odd positive integers equals n squared.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[36] The sum of powers of 2 from 2^0 to 2^n equals 2^(n+1) - 1 for any natural number n.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4
[37] The sum of powers of 2 from 2^0 to 2^n equals 2^(n+1) - 1 for any natural number n.: Verification: Formal proof verified. Formally proven (Lean4). Manifest· Lean4

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.