Working with GPT-5.6 Sol, parallel agents, exact-arithmetic programs and a proof assistant, I attacked two hard problems over two days. One resisted every route I tried. The other produced a proof candidate: a conventional argument written out in full, exact checks on selected inputs, a teaching guide and a partial formalisation in Lean.

That second outcome is still a candidate. No specialist has reviewed the argument, its novelty is not established, and Lean checks only its algebraic core rather than the complete theorem. I would not publish it as a new theorem in its current state.

The pattern I took from the weekend is that mathematical experiments are becoming abundant. The Hadamard project closed 44 precisely defined regions of the search space and audited five standard routes to a nonexistence proof. The Maxwell project produced a complete proof candidate with a machine-checked algebraic core. Accepted mathematical knowledge did not get cheaper alongside any of that, because proof, understanding, novelty and independent review are separate obligations, and generating another route settles none of them.

This is a concrete sequel to two earlier ideas. In AI Has Made Research Cheap. Understanding Is Still Expensive, I argued that AI was making experimentation far cheaper than understanding. In From Tokens to Theorems: Building a Neuro-Symbolic AI Mathematician, I built a simple neuro-symbolic loop in which an LLM proposed mathematical formulas, SymPy checked them exactly, and failed candidates became feedback for the next attempt. That experiment was deliberately modest, but it exposed an architecture that reappeared here at a much larger scale.

Over this weekend, the same pattern extended beyond symbolic sequence problems. Instead of one model and one symbolic checker, I used parallel agents, exact-arithmetic programs, adversarial critics and a proof assistant. Candidate constructions and arguments were generated, attacked, checked where possible and either discarded or retained with an explicit status. The loop had become richer as AI systems improved through 2025 and 2026, but its basic structure remained the same.

Looking back afterwards, I realised the workflow closely resembled a broader pattern that Jeff Dean recently described for science and engineering. Rather than viewing AI as a tool for solving one problem at a time, he characterised research itself as a recurring cycle: propose an experiment, implement and run it, evaluate the result, then use that evaluation to generate a better experiment. His argument was that AI should automate this entire loop, reducing iteration time, running many experiments in parallel and learning from every evaluation.

That was almost exactly what had happened over my weekend, albeit on a much smaller scale. The experiments were mathematical rather than physical. “Implementation” meant exact-arithmetic programs, constraint solvers or proof assistants instead of laboratory equipment. Evaluation meant integer verification, counterexample search and partial formalisation rather than measuring a physical system. Parallel agents proposed constructions, generated verifiers, searched the literature, criticised arguments and translated ideas into different mathematical representations before the next iteration began.

Seen this way, the most striking development was not that AI produced a proof candidate or failed to construct a Hadamard matrix. It was that the experimental cycle itself had become partially automatable. Once exact evaluators existed, proposing, executing and refining mathematical experiments became dramatically cheaper.

The important difference was not simply one of scale but of validation. In the earlier experiment, a candidate formula could be tested directly against the sequence, although reproducing the observed values did not necessarily reveal the underlying mathematics. Here, verification became layered. Exact arithmetic could reject incorrect constructions, Lean could certify parts of an argument, and literature searches could help establish prior work, but none could alone determine novelty, validate every bridge in a universal proof or decide whether a result deserved to become accepted mathematical knowledge.

Hadamard 668 resisted an exact search stack

The first problem asks for a 668 by 668 grid filled only with +1 and -1, arranged so that any two different rows cancel out completely: multiply them entry by entry, add up the result, and you must get exactly zero. In linear-algebra terms, the rows are mutually orthogonal. This is a Hadamard matrix of order 668, and matrices of this kind show up in error-correcting codes, signal processing and the design of experiments. According to Epoch AI’s current catalogue of the problem, 668 is the smallest order for which nobody knows whether one exists.

This is an appealing target for computation because a proposed answer is easy to check. Multiply the candidate by its own transpose using exact integers, then read off the result: every diagonal entry must be 668 and every other entry exactly zero. That is a single matrix multiplication, and there is no subjective judgement at the final gate.

Finding one is another matter. The grid has 446,224 entries and each is either +1 or -1, so a naive search has 2⁴⁴⁶,²²⁴ candidates to get through. No amount of compute touches a number that size. All the useful work goes into not searching it, by imposing enough structure that the number of free choices collapses.

That collapse is what the known construction families buy you. The main route here uses the fact that 668 is 4 times 167. Find four short +1/-1 sequences, of lengths 84 and 83, whose correlation errors cancel at every offset, and a standard recipe assembles them into the full matrix. That recipe is implemented in the repository and was checked end to end on the smaller orders 28 and 36, where exact integer checks confirm the resulting matrices. This takes the search from 2⁴⁴⁶,²²⁴ candidates down to 2³³⁴. Still far too many to enumerate, which is the honest reason the problem is open, but now small enough that structure and symmetry arguments can bite.

Other routes go through different families, each with its own name: Legendre pairs of length 333, Williamson-type quadruples, cocyclic and transposed-Ito constructions over groups of order 167, and difference families with prescribed symmetries. The names are safe to skim past if they are unfamiliar. What matters is that each is a different way of trading one enormous unstructured search for a small structured one, and that each carried exact verifiers for the intermediate objects it accepted. Failed candidates were rejected by integer arithmetic, not by approximate similarity.

Several of the exclusions are precise enough to state numerically. A correlation bound proves that no solution lies within Hamming distance 31 of one particular 334-bit starting point: flipping any 31 or fewer of its bits cannot reach a valid answer. The review bundle will include its full bit strings and digest. Separately, an exact enumeration covers all 4,096 quadruples built from circulant sequences, the ones where each row is the previous row rotated by a single position, restricted to those whose pattern of negative entries survives multiplying every index by 2 modulo 167. None of them works.

A counting argument over odd and even positions rules out one more shape: the case where the third and fourth sequences are the first two with the sign of every other entry flipped. Each of these exclusions covers only the neighbourhood or symmetry pattern it names, and nothing beyond it.

The project also worked the problem from the other side and tried to prove that no such matrix exists in this family. That failed too, and the failure is specific enough to be useful. Nonexistence results in this area draw on a standard toolkit, and the audit worked through it item by item: Leung-Schmidt field descent, ideal factorisation and 2-adic valuation, Hasse-Minkowski, the multiplier theorems, and Bruck-Ryser-Chowla. Here too the names matter less than the outcome. Every one either fails to apply at these parameters or applies and produces no obstruction. What remains is a short list of unresolved mathematical questions; none of these five standard routes supplies the missing obstruction.

Calibration mattered more than any single run. The constraint solver was given a much smaller instance of the same four-sequence problem, one already known to have a solution: sequences of length 15 and 14, against the target’s 84 and 83. It did not find that known solution within two minutes. The timeout proved nothing about the feasibility of either instance. It showed that this solver setup could not solve even the smaller instance within the two-minute calibration budget, so I stopped treating longer runs of the same setup as the main route forward.

By the end, every closed region of the search space had been documented, together with an explicit list of nine remaining open questions. Several promising heuristics proved ineffective. No Hadamard matrix of order 668 was found, and nothing here advances the general conjecture. The problem remains open, and the eventual construction may lie in a family this project never explored. Even so, the journey was immensely rewarding. Exploring new mathematics alongside an AI, applying known techniques to a longstanding open problem, gave a glimpse of higher mathematics becoming increasingly accessible and opening the door for more people to participate in mathematical discovery.

Maxwell’s problem produced a candidate that is much harder to check

The second project began with an old problem from mathematical physics. Place some point charges in space. Their combined potential creates equilibrium points where the forces balance. The goal is to bound how many such points there can be.

The general story changed recently. A July 2026 paper by Arathoon, Ball and Kvalheim constructed five point charges with at least 24 nondegenerate equilibria, disproving Maxwell’s proposed general formula of (k − 1)² for k charges. A second July paper by Gabrielov, Novikov, Novikov and Shapiro sharpened the bound for three positive charges from twelve to six nondegenerate equilibria, for every positive Riesz exponent. Both papers are available on arXiv: The Maxwell Conjecture is False and From 12 to 6: Sharpening the Three-Charge Bound in Maxwell’s Problem.

The exact candidate claim starts with three distinct source points in Euclidean space of dimension at least two, three positive charges and a positive exponent α. Their potential at a point p away from the sources is:

The candidate claim is that this potential has at most four nondegenerate equilibrium points for every α > 0. It treats collinear sources separately and claims exactly two equilibria there. The familiar Coulomb potential is the case α = ½. That is below the bound of six the July paper establishes, which is why the argument needs a specialist reader, not my own confidence in it.

The geometric idea behind the candidate can be described without the technical machinery. For three noncollinear charges, every equilibrium lies inside their triangle. Its position can be represented by three positive weights, called barycentric coordinates. The candidate argument rewrites the physical problem as a question about the peaks of a related mathematical surface.

If two of the relevant peaks existed, draw the straight chord joining them. Both endpoints would have to curve downwards along that chord. The candidate argument derives exact formulae for those two endpoint curvatures and uses a moment inequality to show that they cannot both be negative. If every bridge in that argument is sound, this leaves at most one nondegenerate local minimum of the physical potential inside the triangle. A planar index count then gives the proposed upper bound of four equilibria.

The two projects require different validation. A single proposed Hadamard matrix can be settled by one exact calculation. The Maxwell candidate concerns every source triangle, every set of positive charges and every positive exponent, so it depends on a chain of quantified geometric, analytic and topological steps. A plausible proof can hide an error in any bridge between them.

The conventional manuscript has been checked internally. Exact rational programs evaluate its derived identities on nonsymmetric rational inputs at α = ½ and α = 1. These are exact transcription controls on selected examples, not a symbolic verification of the quantified identities.

The partial Lean development completed successfully, and a source scan found no sorry, admit or added axiom. Its 33 named theorems cover the central moment inequality, endpoint-gap algebra and an abstract two-dimensional Hessian sign argument. They do not yet formalise the barycentric correspondence, the differential identities linking the physical problem to the abstract matrices, the endpoint-curvature derivation, the global index and compactness arguments, or the collinear and higher-dimensional reductions. Lean is checking the algebra, and only the algebra.

That boundary matters. Formalising the algebra that Lean accepts most readily can create an undeserved halo of confidence around the unformalised geometry. The next formalisation target should prioritise the steps most likely to contain an error.

The research loop became partially automatable

I used the model as one component in a research harness, alongside exact programs, a proof assistant and explicit evidence rules. The initial exploration ran over a weekend, followed by additional checking and writing. I selected the problems, redirected or stopped unproductive routes, required the status labels and decided which claims could appear here. Fresh-context critics received an artefact and an adversarial checklist instead of the whole working conversation. The planned public bundle will record the model configuration, prompts, code versions and commit hashes needed for a fuller provenance trail.

One agent proposed formulations. Another tried to break them. Others wrote exact verifiers, searched for counterexamples, translated bounded questions into constraint systems, compared an argument with the literature, or explained an unfamiliar definition from several directions. The work accumulated through a repeatable loop:

• state a precise claim;
• derive consequences;
• test small or finite cases exactly;
• ask a fresh-context critic to attack the weak points;
• formalise the portions where machine checking adds confidence;
• update the status ledger;
• keep, revise or discard the idea.

Inside this particular harness, generating another plausible route was fast relative to checking it. Recording its exact scope, locating its weakest inference, checking whether it was already known and deciding whether it deserved expert attention remained expensive.

That loop could run across many branches in parallel. A failed approach no longer consumed an entire evening before I learnt that its assumptions were inconsistent. A conjectured identity could be turned into an exact program and falsified quickly. A dense proof could be rewritten as a geometric picture, then as algebra, then as a list of obligations for formalisation. The Hadamard project therefore left a useful record even though it missed its target: precise reductions, closed regions, failed techniques and calibration results that can prevent the same blind searches from being repeated.

This is not a conveyor belt working through a finite list of open problems. Proving a theorem changes the surrounding map. It exposes new structures, suggests conjectures, connects questions that had looked unrelated and creates new directions to explore. Mathematical research is cyclical: a result closes one question while opening several others. Making each turn of that cycle cheaper can produce more mathematics to investigate, not an approaching end to the subject.

The model also accelerated learning

I came to both projects without specialist training in their underlying mathematics. Over the weekend I ran into aperiodic autocorrelation, algebraic norms, barycentric coordinates, Hessians, moment inequalities and planar index theory.

The model explained each idea repeatedly and from different angles. It moved between formulae, small numerical examples, visual intuition and the role an idea played in the wider argument. When an explanation did not land, I could say so without embarrassment and ask for another. Eventually several pieces clicked into place.

Before the weekend, I realised, I had subconsciously viewed mathematical research largely as solving problems already waiting on a list. The work itself felt different. Much of it consisted of learning unfamiliar ideas, following failed routes far enough to understand why they failed, reformulating questions and noticing unexpected connections. A proof was one milestone in that larger exploratory process, not the process as a whole.

The outcome was working literacy rather than expertise. I could follow the structure well enough to ask better questions, notice when two claims had been conflated and understand what an external reviewer would need to inspect. A clear explanation still provides no evidence that a theorem is true, and I had to keep reminding myself of the difference between following an argument and being able to reconstruct it.

For me, this was the most immediate form of mathematical abundance. The model met me at the point where understanding stopped and kept changing the representation until progress resumed. It made an unfamiliar subject explorable without making me a specialist in it.

In Mathematicians are grappling with the possibility that AI might eclipse them for Understanding AI, Kai Williams reports on interviews with more than twenty mathematicians. What he heard most often was not models proving things, but models used to find a way into unfamiliar areas of the literature. That matches my experience exactly. The model supplied a map and several translations; the underlying papers, derivations and exact checks still had to carry the claim.

Tasmin Chu’s essay Mathematicians need to act identifies a risk in the same workflow. She argues that the modest extensions, literature exercises and first proofs most exposed to automation are also how students become researchers. If a model does that work instead of directing it, the field may weaken that pipeline. My own extension of her point is that it is also where future reviewers learn judgement. One weekend cannot settle the concern. I learnt most when I had to reconstruct an argument, ask what would falsify it and discover why an explanation had failed to land, not when I simply received an answer.

Larger projects show the same uneven automation

Two much bigger efforts point the same way.

In 2025, Google DeepMind reported that AlphaEvolve had been applied to more than 50 open mathematical problems. According to DeepMind, it rediscovered the best known solution in roughly three quarters of the cases and improved the best known result in about a fifth. The method applies to a useful but narrow class of problems whose proposed solutions can be expressed as algorithms and scored automatically.

In May 2026, OpenAI reported that a general-purpose model found a counterexample to the Erdős unit distance conjecture. Nine external mathematicians then produced a short, digested, human-verified version of the argument, which put the human verification into the published record rather than leaving it as a claim about the model.

Both examples show that automation is uneven. Machine-readable scoring lets a system reject bad candidates and iterate without waiting for a person to read each one. A universal proof candidate still requires careful work on concepts, translations and quantified arguments.

Tom Zahavy’s ICML 2026 position paper LLMs can’t jump offers a vocabulary for that split. Borrowing Peirce’s three modes of inference, he argues that machine learning has mechanised induction, which finds a rule by compressing many examples, and is rapidly mechanising deduction, which derives consequences from premises already fixed. What it has not mechanised is abduction: proposing the premise itself to explain something surprising. His case study is general relativity, and his central observation is that Newtonian gravity faced no measurable crisis at the time. The equivalence of inertial and gravitational mass had been checked to a precision of10⁻⁹, and the one anomaly, Mercury’s orbit, was widely attributed to an undiscovered planet. An optimiser would have found almost nothing to improve. He grants that a model given Einstein’s 1915 postulates could plausibly derive the field equations, since that part is deduction; the 1913 version failed because the axioms were wrong, not because the logic was.

The paper is a position piece and says so, and Zahavy is explicit that his argument is aimed at the physical sciences, where the raw material is sensory, and that mathematics grounds its intuitions differently. I would not push the analogy past that. But the division of labour was recognisable from the inside. The exact programs and Lean did deductive work well, and the Maxwell candidate progressed because a framing already existed to deduce within. Hadamard 668 had no such framing to hand, and what it lacks is not more search but a premise: a construction family or a theorem nobody has written down. His reading of AlphaEvolve makes the same point from the other side: it optimises well inside a fixed framework because it has a gradient to follow.

The pace has not slowed since. Williams opens his article with a Fields Medallist joining OpenAI’s safety team and an internal model that the company says solved ten major open problems; Chu opens hers with the same announcement, noting that the reported token cost of those results was around two thousand dollars. I have not checked either claim, and neither had been through review when I wrote this.

Jordan Ellenberg captured the optimistic historical response in his 2014 book How Not to Be Wrong, in a passage Williams quotes: “We’ll reclassify that research as ‘computation.’” Mathematics has repeatedly moved its frontier after machines absorbed an old task. Reclassification does not, by itself, explain how people will learn to choose the next questions, judge the answers or sustain a community around them.

AI may therefore increase mathematical abundance in a broader sense than proving more theorems. It may generate more conjectures, partial theories, proposed connections between fields and directions worth investigating. My weekend does not establish how often those suggestions will be deep or genuinely new; it shows only how cheaply candidate routes can already be generated and tested. Even a modest increase would shift more of the burden toward understanding, curation, review, explanation and prioritisation. The challenge is not only to produce more mathematics, but to decide what deserves attention.

Jeff Dean, in founding Discoveryloop, frames this as a programme extending far beyond mathematics. Fusion, medicine, cybersecurity and materials science all share a version of the same experimental cycle: propose an experiment, run it, evaluate the result and use that evaluation to choose the next experiment. If AI increasingly automates that loop across science and engineering, mathematics may be an early illustration of a broader transition rather than a special case. The bottleneck then moves from generating experiments to deciding which outputs are reliable, significant and worthy of becoming trusted knowledge.

Abundance creates a human and institutional problem

If models can generate many more conjectures, proof candidates, counterexamples and partial formal developments than humans can read, storing them in chat transcripts will not work. The same acceleration also changes who learns the craft, who receives credit, who takes responsibility for errors and who is asked to review the output.

A useful mathematical record needs more than a title and a PDF. It should carry a normalised statement, explicit assumptions, a status label and the precise scope of any computation. It should also carry the formal artefacts where they exist, the dependencies on earlier results, the provenance of the human and machine contributions, the novelty status, the known attacks and a plain-language explanation.

Search should operate over claims and dependencies rather than only keywords. A useful system could match a proposed lemma against equivalent statements in different notation, show which unreviewed claims would imply a target result, and identify arguments that rely on the same unformalised bridge. Failed routes should be searchable too, provided their scope is exact. Over time, this could become a shared corpus of successful proofs, failed attempts, abandoned search branches, reductions, counterexamples, calibration results and intermediate constructions. Every well-scoped failure could narrow the remaining search space instead of being unknowingly repeated.

Without that infrastructure, I expect repeated work and misplaced confidence. Models will rediscover old results, subtly vary false proofs and generate more material than peer review can absorb. The bottleneck would move from producing mathematics to curating a trustworthy map of it.

Williams’s interviews were reporting, not a representative survey, and the people he spoke with offered no single response. Many expected AI to complement their work in the near term and already used it in limited ways, especially to traverse unfamiliar literature. Others worried about the training path for younger researchers, future funding and a profession organised around tasks that models may learn to perform. Their disagreement reflects several goals being bundled together. Solving open problems is one aim of mathematics, but so are understanding, explanation, theory-building, teaching and sustaining a community.

The Leiden Declaration warns that current automated techniques produce plausible but unreliable arguments that are hard to distinguish from correct proofs, that the same problem applies to formalisations through the translation between machine and human presentations, and that AI-assisted papers make reviewing more demanding. Timothy Gowers, writing about the declaration, pushes the thought further: he imagines mathematicians selecting from a vast body of AI-generated mathematics and writing it up so that others can absorb it, and he is candid about how much of the current culture that would displace.

Any such map will need reputation and incentives behind it. Gowers makes the point sharply: if one person gets a model to solve an open problem and another digests the solution and explains it so that mathematicians can learn from it, the second person should get most of the credit. Explaining why a generated result matters, finding the subtle flaw in it, or connecting it to a neglected theorem may be worth more than producing the first draft. Today’s publication culture is not designed to recognise those contributions cleanly.

The attribution problem reaches further back than the final proof. Many celebrated breakthroughs are the culmination of decades of definitions, lemmas, conjectures, failed approaches and techniques developed by many researchers. If an AI supplies the last missing argument, rewarding only that last mile risks obscuring the human work that made the step possible and gave it meaning. Provenance should therefore record not only who or what completed the proof, but the chain of ideas and results on which it depends. Credit should follow that chain rather than collect at its endpoint.

Chu’s essay sharpens all of this into an institutional argument. She presents accurate attribution, responsibility for mistakes and open knowledge as mathematical values that AI use may strain. A generated proof can obscure the human work it depends on, and a plausible error can consume far more expert attention than it took to produce. She also worries that researchers will share fewer unfinished ideas if somebody else can convert those ideas into model-assisted results before their originators finish. That last point is a forecast rather than something my experiment demonstrates, but it means a claim registry would need rules for consent and attribution around unpublished ideas, not only better search over finished ones. Among the prescriptions she draws from that are that mathematicians should use models judiciously or not at all, and that chat logs should be published alongside mathematical papers.

Independent review would be the next natural step

I do not intend to turn this personal weekend learning project into a public review effort. If I did, I would first establish the literature and priority position, invite specialists to attack the conventional argument, and formalise the steps most susceptible to undetected error. Until those gates are passed, it remains a proof candidate.

For Hadamard 668, a final exact verifier has been written but has not yet been exercised on a genuine candidate. The missing ingredient is a new structural construction or theorem. The negative record should guide future attempts without being mistaken for a solution or a nonexistence proof.

Whether or not either project goes further, the durable object is not a proof alone but its place on the map. A proof sitting on a server has surprisingly little value if nobody knows it exists, why it matters, how it relates to previous work or whether it can be trusted. As mathematical artefacts multiply, navigation through them becomes the scarce resource: locating the relevant claim, understanding its dependencies, judging its status and explaining where it changes the frontier.

Running the loop faster does not close that gap. Cheap experiments multiply the things we can check and the questions we can ask; they do not, on their own, tell us which premises are worth checking or turn an output into shared understanding. Experiments become cheap. Knowledge does not.

Disclaimer: This was an informal, curiosity-driven project undertaken in my personal time. The views expressed here are my own and do not represent those of my employer or any affiliated organisation. The content is based on personal experience and reflection, and should not be taken as professional or academic advice.

📚References

• Gabrielov, A., Novikov, Dm., Novikov, T., & Shapiro, B. (2026). From 12 to 6: Sharpening the Three-Charge Bound in Maxwell’s Problem. Proves
  that three positive point charges admit at most six nondegenerate equilibria for every positive Riesz exponent, improving the twelve-point bound from the authors’ earlier work by supplying a separation argument at the saddle of a separated-variable first integral. This is the published bound the proof candidate discussed here would sit below, and the reason that candidate needs a specialist reader rather than my own confidence in it.
• Arathoon, P., Ball, G., & Kvalheim, M. D. (2026). The Maxwell Conjecture is False. Exhibits five point charges whose electrostatic potential has at least 24 critical points, all nondegenerate, refuting Maxwell’s proposed bound of (k−1)² for k charges. Together with the paper above it defines the state of Maxwell’s problem in July 2026, which is the setting for the four-equilibrium claim described here.
• Zahavy, T. (2026). Position: LLMs can’t jump. ICML 2026, PMLR 306. Argues via Peirce’s three modes of inference that machine learning has mechanised induction and is rapidly mechanising deduction, but not abduction — the invention of the premise itself — using general relativity as a case study in which no error signal existed for an optimiser to follow. Supplies the vocabulary this article uses to separate the deductive work Lean did well from the missing premise that keeps Hadamard 668 open.
• Chu, T. (2026, 2 August). Mathematicians need to act. Sets out attribution, accountability for error and open knowledge as community values that AI use may strain, argues that the tractable problems most exposed to automation are also how research mathematicians are trained, and takes the position that in the current climate it is unethical to ask a model to prove a new theorem. The standard against which this project is measured in the closing section.
• Williams, K. (2026, 4 August). Mathematicians are grappling with the possibility that AI might eclipse them.Understanding AI. Reporting from the International Congress of Mathematicians based on conversations with over twenty mathematicians, finding the most common use to be navigating unfamiliar areas of the literature rather than proving results, and quoting the passage from Ellenberg’s How Not to Be Wrong reproduced here.