Mathematical Proofs & Shared Intelligence

1. Framing Intelligence as a Continuum

Intelligence is most usefully understood as a continuum of capacities—pattern recognition, abstraction, search, formal verification, and creative hypothesis generation—rather than as a set of discrete, species-bound categories. Human intelligence (HI) and machine intelligence (MI) are overlapping distributions on that continuum.

They are not sealed boxes with fixed boundaries.

Under ordinary set-theoretic language one can list four mutually exclusive possibilities: HI and MI share some capacities; they share none; HI is a proper subset of MI; or MI is a proper subset of HI. Present evidence points most strongly to the first of these. Formal theorem-proving, exhaustive case analysis, algebraic simplification, and the verification of large but finite combinatorial statements are already performed by both humans and machines. Claims of empty intersection, or of one form of intelligence being wholly contained in the other, are not supported by current practice.

2. Proving and Disproving Conjectures

The work of proving or disproving a mathematical conjecture is not a single point on the continuum; it is a cluster of related activities that already occupy the overlapping region. Search and verification. Exhaustive or heuristic exploration of a problem space, followed by formal checking, is the part of the work in which machines already dominate for many classes of problem. Classic examples include the four-color theorem, the Kepler conjecture (completed in the Flyspeck project), the Boolean Pythagorean triples problem, and numerous results in combinatorial and finite-group theory. In these cases humans typically supply high-level strategy or the initial formalization; machines supply the brute-force or automated reasoning that finishes the proof.

Insight and conceptual leap. Finding the right definition, invariant, or reduction that renders a problem tractable remains predominantly a human contribution. Yet machine systems—neural conjecture generators, reinforcement-learning guided search, and large language models that propose candidate lemmas—are beginning to contribute ideas that humans then filter and formalize. The boundary is therefore shifting rather than fixed. Interpretation and communication. Explaining why a proof works, relating it to broader mathematical structure, and deciding which conjectures are worth pursuing. remain almost entirely human activities at present. These higher-level judgments sit further toward the human end of the continuum, but they are not required for the existence of a correct formal proof.

Taken together, the activity of conjecture resolution is already shared. Different sub-skills simply occupy different points along the continuum.

3. Are There Exclusive Proofs?

A natural further question is whether any mathematical proof is possible only for humans, or only for machines. The answer, on present evidence, is no.

No known proof that only a human can produce. Any finite formal proof written in a standard foundational system (ZFC, type theory, or similar) is in principle checkable by a machine. If a human has produced a correct proof, a sufficiently capable automated theorem prover or proof assistant can, given enough time and guidance, reconstruct or verify an equivalent formal version. Claims that “only humans can do this” usually collapse either to the current practical limitations of existing provers or to the informal narrative that accompanies the formal argument—not to an absolute barrier.

No known proof that only a machine can produce. Every machine-generated proof that mathematicians have accepted has been, or could in principle be, inspected, understood, and re-derived by humans, even when the inspection is tedious. Extremely long machine proofs can be compressed, modularized, or given higher-level human explanations; they do not remain permanently opaque. The four-color theorem and the Kepler conjecture again serve as illustrations: the computer performed the heavy case analysis, yet the overall architecture and the residual human-checkable parts were supplied by people.

In short, the set of mathematical statements that possess formal proofs is the same set whether those proofs are discovered by humans, by machines, or by collaboration. The continuum difference is practical—speed, scale, memory, and the balance between search and insight—not an ontological separation into “human-only” and“machine-only” theorems.

4. The Interesting Frontier

The interesting question is therefore not the existence of exclusive proofs, but the shifting ratio of insight versus search inside the shared region of the continuum. As machine systems improve at proposing the conceptual moves that used to be purely human, that ratio will continue to change. The continuum itself remains the most accurate map: overlapping capacities, no clean partition, and a frontier that moves with every advance in automated reasoning