The definition of major conjecture for the purposes of this market is one of the 129 "open problems" in this Wikipedia article as of 1 August 2025: https://en.wikipedia.org/wiki/List_of_conjectures
If a valid proof found by an AI is posted, then all years after the posting date will resolve YES.
The proof has to be accepted by a majority of the mathematical community (this market will stay open for a significant amount of time after a claimed proof to allow for disputes to arise).
It does not count if the problem was solved by a human beforehand.
If the proof was a human-AI collaboration, that is likely not sufficient for a YES-resolution, unless an overwhelming amount of the work (>90%) was done by the AI. If the AI produces an essentially complete proof, but humans reformulate the proof into easier-to-read prose, that would be sufficient.
Traditional AI like SAT-solvers/SMT-solvers count as AIs for the purposes of this market, but any problem translation or tinkering with these tools count as human work (if performed by humans). I will likely not count problems that only involve such tools, since there is usually still a lot of human work needed for such proofs (e.g. proofs of the empty hexagon number or the pythagorean triple coloring problem).
A few weeks after the start of a year, if I haven't found a proof claim and none has been posted in the comments, that year will resolve NO.
I will not bet on this market
1,000For future record, the 129 conjectures that count are the following.
1/3–2/3 conjecture, abc conjecture, Agoh–Giuga conjecture, Agrawal's conjecture, Andrews–Curtis conjecture, Andrica's conjecture, Artin conjecture (L-functions), Artin's conjecture on primitive roots, Bateman–Horn conjecture, Baum–Connes conjecture, Beal's conjecture, Beilinson conjecture, Berry–Tabor conjecture, Big-line-big-clique conjecture, Birch and Swinnerton-Dyer conjecture, Birch–Tate conjecture, Birkhoff conjecture, Bloch–Beilinson conjectures, Bloch–Kato conjecture, Bochner–Riesz conjecture, Bombieri–Lang conjecture, Borel conjecture, Bost conjecture, Brennan conjecture, Brocard's conjecture, Brumer–Stark conjecture, Bunyakovsky conjecture, Carathéodory conjecture, Carmichael totient conjecture, Casas-Alvero conjecture, Catalan–Dickson conjecture on aliquot sequences, Catalan's Mersenne conjecture, Cherlin–Zilber conjecture, Chowla conjecture, Collatz conjecture, Cramér's conjecture, Conway's thrackle conjecture, Deligne conjecture, Dittert conjecture, Eilenberg−Ganea conjecture, Elliott–Halberstam conjecture, Erdős–Faber–Lovász conjecture, Erdős–Gyárfás conjecture, Erdős–Straus conjecture, Farrell–Jones conjecture, Filling area conjecture, Firoozbakht's conjecture, Fortune's conjecture, Four exponentials conjecture, Frankl conjecture, Gauss circle problem, Gilbert–Pollack conjecture on the Steiner ratio of the Euclidean plane, Gilbreath conjecture, Goldbach's conjecture, Gold partition conjecture, Goldberg–Seymour conjecture, Goormaghtigh conjecture, Green's conjecture, Grimm's conjecture, Grothendieck–Katz p-curvature conjecture, H conjecture, Hadamard conjecture, Herzog–Schönheim conjecture, Hilbert–Smith conjecture, Hodge conjecture, Homological conjectures in commutative algebra, Hopf conjectures, Ibragimov–Iosifescu conjecture for φ-mixing sequences, Invariant subspace problem, Jacobian conjecture, Jacobson's conjecture, Kaplansky conjectures, Keating–Snaith conjecture, Köthe conjecture, Kung–Traub conjecture, Legendre's conjecture, Lemoine's conjecture, Lenstra–Pomerance–Wagstaff conjecture, Leopoldt's conjecture, List coloring conjecture, Littlewood conjecture, Lovász conjecture, MNOP conjecture, Manin conjecture, Marshall Hall's conjecture, Mazur's conjectures, Montgomery's pair correlation conjecture, n conjecture, New Mersenne conjecture, Novikov conjecture, Oppermann's conjecture, Petersen coloring conjecture, Pierce–Birkhoff conjecture, Pillai's conjecture, De Polignac's conjecture, Quantum PCP conjecture, quantum unique ergodicity conjecture, Reconstruction conjecture, Riemann hypothesis, Ringel–Kotzig conjecture, Rudin's conjecture, Sarnak conjecture, Sato–Tate conjecture, Schanuel's conjecture, Schinzel's hypothesis H, Scholz conjecture, Second Hardy–Littlewood conjecture, Selfridge's conjecture, Sendov's conjecture, Serre's multiplicity conjectures, Singmaster's conjecture, Standard conjectures on algebraic cycles, Tate conjecture, Toeplitz' conjecture, Tuza's conjecture, Twin prime conjecture, Ulam's packing conjecture, Unicity conjecture for Markov numbers, Uniformity conjecture, Unique games conjecture, Vandiver's conjecture, Virasoro conjecture, Vizing's conjecture, Vojta's conjecture, Waring's conjecture, Weight monodromy conjecture, Weinstein conjecture, Whitehead conjecture, Zauner's conjecture