Search arXivSearch

arXiv subjects

Codrut Grosu

Publications and source records attributed to Codrut Grosu.

9 recordsLinked to original sources

Advancing Mathematics Research with AI-Driven Formal Proof Search

Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method's ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erd\H{o}s problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erd\H{o}s successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.

cs.AI

Almost all trees are almost graceful

The Graceful Tree Conjecture of Rosa from 1967 asserts that the vertices of each tree T of order n can be injectively labelled by using the numbers {1,2,...,n} in such a way that the absolute differences induced on the edges are pairwise distinct. We prove the following relaxation of the conjecture for each c>0 and for all n>n_0(c). Suppose that (i) the maximum degree of T is bounded by O(n/log n), and (ii) the vertex labels are chosen from the set {1,2,..., (1+c)n}. Then there is an injective labelling of V(T) such that the absolute differences on the edges are pairwise distinct. In particular, asymptotically almost all trees on n vertices admit such a labelling. As a consequence, for any such tree T we can pack (2+2c)n-1 copies of T into the complete graph of order (2+2c)n-1 cyclically. This proves an approximate version of the Ringel-Kotzig conjecture (which asserts the existence of a cyclic packing of 2n-1 copies of any T into the complete graph of order 2n-1) for these trees. The proof proceeds by showing that a certain very natural randomized algorithm produces a desired labelling with high probability.

math.CO

On spanning trees with high internal degree

Alon and Wormald showed that any graph with minimum degree d contains a spanning star forest in which every connected component is of size at least \Omega((d/\log d)^{1/3}). They asked if any connected graph with minimum degree at least d has a spanning tree in which every internal vertex has degree at least cd/\log d, for some absolute constant c > 0. We give a simple example showing that this is not the case.

math.CO

A note on projective norm graphs

The projective norm graphs P(q, 4) introduced by Alon, R\'onyai and Szab\'o are explicit examples of extremal graphs not containing K_4,7. Ball and Pepe showed that P(q, 4) does not contain a copy of K_5,5 either for q >= 7, asymptotically improving the best lower bound for ex(n, K_5,5). We show that these results can not be improved, in the sense that P(q, 4) contains a copy of K_4,6 for infinitely many primes q.

math.CO

A new lower bound for the Towers of Hanoi problem

More than a century after its proposal, the Towers of Hanoi puzzle with 4 pegs was solved by Thierry Bousch in a breakthrough paper in 2014. The general problem with p pegs is still open, with the best lower bound on the minimum number of moves due to Chen and Shen. We use some of Bousch's new ideas to obtain an asymptotic improvement on this bound for all p >= 5.

math.CO

On the algebraic and topological structure of the set of Tur\'an densities

The present paper is concerned with the various algebraic structures supported by the set of Tur\'an densities. We prove that the set of Tur\'an densities of finite families of r-graphs is a non-trivial commutative semigroup, and as a consequence we construct explicit irrational densities for any r >= 3. The proof relies on a technique recently developed by Pikhurko. We also show that the set of all Tur\'an densities forms a graded ring, and from this we obtain a short proof of a theorem of Peng on jumps of hypergraphs. Finally, we prove that the set of Tur\'an densities of families of r-graphs has positive Lebesgue measure if and only if it contains an open interval. This is a simple consequence of Steinhaus's theorem.

math.CO

On the rank of higher inclusion matrices

Let r >= s >= 0 be integers and G be an r-graph. The higher inclusion matrix M_s^r(G) is a {0,1}-matrix with rows indexed by the edges of G and columns indexed by the subsets of V(G) of size s: the entry corresponding to an edge e and a subset S is 1 if S is contained in e and 0 otherwise. Following a question of Frankl and Tokushige and a result of Keevash, we define the rank-extremal function rex(n,t,r,s) as the maximum number of edges of an r-graph G having rank M_s^r(G) <=\binom{n}{s} - t. For t at most linear in n we determine this function as well as the extremal r-graphs. The special case t=1 answers a question of Keevash.

math.CO

F_p is locally like C

Vu, Wood and Wood showed that any finite set S in a characteristic zero integral domain can be mapped to F_p, for infinitely many primes p, while preserving finitely many algebraic incidences of S. In this note we show that the converse essentially holds, namely any small subset of F_p can be mapped to some finite algebraic extension of Q, while preserving bounded algebraic relations. This answers a question of Vu, Wood and Wood. We give several applications, in particular we show that for small subsets of F_p, the Szemer\'edi-Trotter theorem holds with optimal exponent 4/3, and we improve the previously best-known sum-product estimate in F_p. We also give an application to an old question of R\'enyi. The proof of the main result is an application of elimination theory and is similar in spirit with the proof of the quantitative Hilbert Nullstellensatz.

math.CO

The extremal function for partial bipartite tilings

For a fixed bipartite graph H and given number c, 0<c<1, we determine the threshold T_H(c) which guarantees that any n-vertex graph with at edge density at least T_H(c) contains $(1-o(1))c/v(H) n$ vertex-disjoint copies of H. In the proof we use a variant of a technique developed by Komlos~\bcolor{[Combinatorica 20 (2000), 203-218}]

math.CO