Mathematical Research

Autonomous conjecture generation and formal verification from axioms. 206 with computational evidence. 42 falsified. 177 lemmas accumulated.

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

Ramsey

[1] Every 2-coloring of the complete graph K_47 contains a monochromatic complete subgraph K_5, and moreover, any extremal coloring of K_47 avoiding K_5 must have a specific structural property: at least one color class must induce a subgraph where all vertices…: Verification: Computational evidence. Computational evidence; no counterexample in 47 cases. Report·DOI Manifest
[2] 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

[3] For all x >= 1000, the actual count of twin prime pairs up to x strictly exceeds the standard Hardy-Littlewood prediction (2*C2*x/ln(x)^2) but remains bounded above by the prediction augmented with a specific second-order correction term: 2*C2*x/(ln(x)^2 -…: Verification: Falsified. Falsified. Report·DOI Manifest
[4] For any integer n > 1, if n is a perfect power (n = x^a with x, a > 1) and the next consecutive perfect power m (m = y^b with y, b > 1, m > n) satisfies m - n = 1, then n must be 8. Furthermore, for any perfect power n > 8, the gap to the next perfect power…: Verification: Falsified. Falsified. Report·DOI Manifest
[5] For any integer n > 1, let S(n) be the set of odd numbers encountered in the Collatz trajectory of n before reaching 1. Let m = min(S(n)). Then the total stopping time (number of steps to reach 1) is strictly less than m^2 + m.: Verification: Falsified. Falsified. Report·DOI Manifest
[6] For any integer n >= 2, let S_n be the set of primes of the form k^2+1 where k <= n. Let M_n be the maximum gap between consecutive elements in the sorted sequence S_n (defining the first gap as p_1 - 2). Then, M_n is strictly less than (ln(p_max))^3, where…: Verification: Falsified. Falsified. Report·DOI Manifest
[7] For every even integer n > 100, there exists a Goldbach partition n = p + q (with p <= q) such that the prime p lies within the interval [n/2 - sqrt(n), n/2]. Furthermore, the smallest such prime p satisfies the stronger bound: n/2 - p < sqrt(n) / ln(n).: Verification: Falsified. Falsified. Report·DOI Manifest
[8] For every even integer n >= 1000, 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]. Furthermore, the number of such 'central' Goldbach partitions is strictly greater…: Verification: Computational evidence. Computational evidence; no counterexample in 50,000 cases. Report·DOI Manifest
[9] For every even perfect number n > 6, the sum of the binary digits of (n/2) is strictly less than the number of distinct prime factors of (n-1).: Verification: Falsified. Falsified. Report·DOI Manifest
[10] For every integer N >= 100, let T(N) be the count of twin prime pairs (p, p+2) with p <= N, and let S(N) be the sum of the reciprocals of the smaller primes in these pairs (i.e., sum(1/p) for all such p). The conjecture states that the ratio R(N) = T(N) /…: Verification: Falsified. Falsified. Report·DOI Manifest
[11] For every integer n >= 3, if the Fibonacci number F_n is prime, then n must be a prime number, AND the index n satisfies the property that 2n+1 is either a prime number or a semiprime (product of exactly two primes, not necessarily distinct). Furthermore, if…: Verification: Falsified. Falsified. Report·DOI Manifest
[12] Let P_N be the set of primes of the form n^2+1 for 1 <= n <= N. Let A_N be the count of such primes where the generator n is itself a prime number. The conjecture states that for all N >= 1000, the ratio of the density of 'prime-generated' primes to the…: Verification: Falsified. Falsified. Report·DOI Manifest

Graph Theory

[13] In any 2-coloring of K_18, the minimum number of monochromatic K_4 is exactly 18, and this minimum is achieved only by colorings where the graph of one color forms a specific structured graph related to the Turán graph T(18,3).: Verification: Falsified. Falsified. Report·DOI Manifest
[14] 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. Report·DOI Manifest

Combinatorics

[15] 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
[16] 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
[17] 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
[18] 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
[19] 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
[20] 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: Computational evidence. Computational evidence; no counterexample in 2,550 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.