A provocative argument by writer Mohamed Abdelmenem says AI-generated mathematical proofs, checked by formal systems such as Lean 4, could make parts of traditional peer review redundant. The bigger question is not whether humans disappear from science, but where human judgment is still needed when a machine can verify the logic.

For generations, mathematics has relied on a familiar process. A researcher develops a proof, other experts examine it, journals assess it, mistakes are challenged and, eventually, the work becomes part of the accepted record.

AI is beginning to complicate that model.

In a recent Medium essay, writer Mohamed Abdelmenem argues that machine-generated mathematical proofs combined with formal verification systems such as Lean 4 could fundamentally change how mathematical work is validated. His headline is deliberately provocative: “OpenAI’s $2,000 Math Proofs Kill Peer Review.”

His central point is less about removing academics altogether and more about what happens when the correctness of a proof can be checked by software rather than trusted primarily because a group of experts has reviewed it.

As he puts it:

Human peer review was a proxy for trust. Cryptographic compilers don’t need proxies.

That is a powerful claim. It is also one that needs some qualification.

From Human Consensus to Machine Verification

Formal proof systems such as Lean are designed to check mathematical arguments against explicit logical rules.

If a proof has been correctly formalised and the verifier accepts it, researchers gain a very strong guarantee that the sequence of logical steps is internally valid.

That is different from asking several mathematicians to read a conventional paper and decide whether the argument appears correct.

Abdelmenem sees this as a fundamental shift in scientific authority. In his framing, the verifier increasingly becomes the arbiter of mathematical correctness.

He writes:

Science is no longer a consensus to be reached. It is a certificate to be compiled.

Whether science as a whole can be described that way is debatable. But within areas that can be completely expressed in formal logic, the argument is harder to dismiss.

The Debate Is Bigger Than a $2,000 AI Bill

The essay centres on claims around an unreleased OpenAI system referred to as Astra, which the author says produced machine-checkable work on several difficult mathematical problems for roughly $2,000 in test-time computing.

Abdelmenem is careful to argue that this headline number should not be mistaken for the total cost of building the intelligence behind the result.

He distinguishes between the cost of running an already-trained model and the far larger cost of training and developing the underlying system.

The inference is cheap. The intelligence is not,” he writes.

That distinction matters well beyond mathematics.

If AI systems become capable of producing valuable research outputs relatively cheaply once trained, companies and universities could begin seeing extraordinary output from extremely expensive underlying infrastructure.

A cheap final proof does not mean cheap AI research.

Does Formal Verification Really Replace Peer Review?

This is where the argument becomes more complicated.

A formal verifier can check whether a proof follows from a set of assumptions. It cannot necessarily decide whether a theorem matters, whether the assumptions are the right ones, whether the result is genuinely novel or whether the work has been framed in the most useful way.

Those remain human questions.

Peer review also does more than test logical correctness. Reviewers assess relevance, originality, methodology, interpretation and the relationship between a new result and existing knowledge.

For mathematics, formal verification could remove a large amount of painstaking checking.

It does not automatically remove the need for mathematical understanding.

A proof might be correct yet uninteresting. Another might depend on a technically valid formulation that obscures the real intellectual problem. A third may deserve attention because it reveals a completely new method rather than simply because the final theorem checks out.

The verifier can answer: “Is this logically valid?”

The scientific community still has to answer: “What does this mean?”

Where AI Could Change Mathematics Most

The strongest case for machine verification is likely to emerge where correctness can be expressed formally.

Mathematics and software verification are obvious examples.

An AI system might generate thousands of possible arguments, discard failed approaches and eventually produce a proof that a formal system can check independently.

In that environment, the AI that discovers the result and the system that verifies it do not even have to be trusted in the same way.

The generative system can be probabilistic and occasionally wrong. The verifier can remain deterministic.

This matters because one of the central weaknesses of generative AI is hallucination. Formal verification provides a way of separating plausible-looking output from output that actually satisfies the required logical constraints.

Abdelmenem argues that this could create a new model for research in which verification becomes part of the computational pipeline rather than something carried out weeks or months later by human reviewers.

But Not Every Field Can Be Compiled

The limitations become obvious once we move outside formal systems.

There is no Lean certificate that can prove the correct interpretation of a historical event.

A compiler cannot determine whether a sociological explanation captures human behaviour adequately.

It cannot formally certify whether a new theory of culture is meaningful, whether an economic model reflects reality or whether a medical study has asked the right clinical question.

Even Abdelmenem acknowledges this boundary. His proposed framework applies to “formal logic domains like mathematics and code compilation,” not to areas such as market research or creative strategy.

That distinction is crucial.

The future may therefore be less about AI killing peer review and more about splitting peer review into different kinds of work.

Machines may increasingly verify what machines can verify.

Humans may spend more time evaluating everything that cannot be reduced to formal proof.

Peer Review Could Become More Valuable, Not Less

There is another possible outcome.

If formal verification removes some of the repetitive burden of checking technical correctness, human reviewers could focus more heavily on interpretation and significance.

That could make peer review faster in some disciplines while also making the remaining human contribution more intellectually demanding.

A reviewer would no longer spend as much time checking whether line 47 follows from line 46.

Instead, the questions become: Is this result important? Does it change the field? Are the assumptions appropriate? What should researchers investigate next?

In that sense, AI may not make human expertise obsolete. It may change what expertise is for.

Academic Institutions Will Still Have to Adapt

What is difficult to imagine is that academic publishing will remain unchanged.

If AI systems can generate large volumes of machine-verifiable research, journals may face an entirely new scale problem.

Human reviewers cannot evaluate an unlimited number of machine-generated submissions using the same processes designed for human researchers producing a handful of papers each year.

Formal certificates could therefore become part of the submission process, especially in mathematics, theoretical computer science and other fields where proofs can be mechanised.

A paper might eventually arrive with two layers of validation: a machine-checkable certificate demonstrating logical correctness and human review assessing novelty, relevance and interpretation.

That would not abolish peer review.

It would turn it into something different.

The Real Question Is What We Mean by “Knowing”

The most interesting part of this debate is philosophical rather than computational.

Scientific communities have traditionally trusted knowledge because other qualified humans could inspect it, challenge it and eventually reproduce or verify it.

Formal systems introduce another model of trust.

Instead of asking whether respected experts agree that a proof is correct, researchers can ask whether the proof survives an explicit logical verification process.

Neither approach is sufficient for every kind of knowledge.

But mathematics may be becoming one of the first fields where the balance shifts dramatically towards machine verification.

Abdelmenem’s argument intentionally pushes this to its extreme conclusion: the compiler becomes the new peer reviewer.

A more realistic possibility is that the compiler becomes one peer reviewer and perhaps the fastest, most unforgiving one science has ever had.

The humans remain, but their job changes.

About the Author

MohamedAbdelmenem writes about artificial intelligence, infrastructure, verification and the economics of emerging technologies on Medium and through MeetCyber.

His essay, OpenAI’s $2,000 Math Proofs Kill Peer Review, argues that the combination of AI-generated research and formal verification could reshape scientific validation, particularly in disciplines built around closed logical systems.