OpenAI maths and Photoshop rebuilt with AI

Tech News, powered by Quinck. A new episode talked through in front of the camera: the video is on our channel, and you'll find it below.

▶ Watch the episode on YouTube

This time there are two stories, plus one question that ties them together. On 6 October OpenAI published hundreds of new mathematical results, many of them certified by a formal proof. In the same week a tiny team put open source clones of Photoshop, Premiere, Word, Excel and AutoCAD on GitHub, written with an AI agent, while social media filled up with Minecraft inside Elden Ring.

They look like unrelated stories. The question in between, why AI is so good at maths specifically, shows they aren't: AI becomes extremely strong wherever the answer can be checked automatically. A proof in Lean either passes the check or it doesn't. A Photoshop clone either produces the same output as the original or it doesn't. A decompiled game either recompiles byte for byte identical, or it doesn't.

In 30 seconds

OpenAI published a repository with hundreds of maths papers: solutions or significant partial advances for around 370 families of results, about 40% with a Lean proof attached, obtained with an average of 3 hours of compute per problem. Around 4,000 problems were submitted, and three results have already been withdrawn.
AI excels at maths because of reinforcement learning, RLVR in particular: the model learns where the answer can be checked automatically. That is why medicine, where verification goes through real-world experiments, moves more slowly.
The same principle is now remaking software. ArtCraft's apps clone half of Creative Cloud, Office and AutoCAD in a week, with Claude Opus 5.5 and Rust. In video games, AI-driven mashups and decompilations are booming. The legal question and the market question are both open.

1. OpenAI publishes hundreds of mathematical results

On 6 October OpenAI published a GitHub repository with hundreds of maths papers: solutions, or significant partial advances, for around 370 families of results. A good share of them, about 40%, come with a proof in Lean, the proof assistant that checks a proof automatically: if it passes, it's correct, and you don't have to trust anyone.

The results come from an internal model that hasn't been released yet. It's the same one that, just over a month ago, led to the solution of the Navier-Stokes problem.

Time and cost: 3 hours of compute per problem

The most obvious objection is about money. According to some estimates, the Navier-Stokes proof cost millions of dollars, with thousands of agents working in parallel. That kind of money pays for a lot of researchers.

A well-funded human team might have reached similar results, although we'll never have the counterfactual. But there are two differences. The first is time: for humans it would have taken years. The second matters more: the vast majority of these new results came out of roughly 3 hours of compute on average.

Two caveats, and they're important:

Around 4,000 problems were submitted. The ones solved are a significant share, but far from all of them.
Results without a Lean certificate may contain errors. Three have already been withdrawn.

Only counterexamples? The objections

You often hear that AI always solves problems the same way: it brute-forces a counterexample and stops there, with none of the ingenuity we associate with a mathematician.

There are two answers. Even when the solution is a counterexample, as with the Jacobian conjecture previously solved by Anthropic or with Navier-Stokes, the path to it is almost never trivial: it isn't a blind search through the space of solutions. And for the October results the objection simply doesn't hold: many of them aren't counterexamples but complex constructions that the mathematicians reviewing them find counter-intuitive.

For a few years it was possible to argue that LLMs didn't really reason. It was a debated position, but a defensible one. Today's systems are something else: logical reasoning is there, and in some domains it already goes beyond human ability.

How mathematicians are taking it

Badly, in part. On social media you'll find PhD students and researchers discovering that the problem they had spent years on was solved overnight. And the question going around is a brutal one: if the value of human beings no longer lies in finding solutions, what is left?

For now, at least two things.

Understanding. Papers written by AI, not to mention the Lean proofs, are extremely hard to read. Someone needs to digest this mass of results, with help from LLMs, and find the intuitive explanations. Knowing that a proposition is true is not the same as understanding it, and it's deep understanding that gives rise to new questions and new branches of research.

Choosing the direction. Even the latest models don't show much creativity in deciding what to study. For now it's humans who choose which problems to point them at. That could change.

Our take: a mathematician is not a calculator

Reducing a mathematician's work to producing solutions is like reducing an engineer's work to writing lines of code. The solution is the measurable output, but the value lies in understanding why it works and knowing which question to ask next. On that front AI helps, for now, but doesn't replace.

Still, this batch of publications is a historic result, a turning point. That is exactly why we need a serious, pragmatic conversation about the role we want human beings to play in mathematics.

2. Why is AI so good at maths?

Let's take a step back. Why are AI labs investing so heavily in maths, rather than in problems with an immediate impact, like medicine?

Put like that it looks like a paradox. They'd have every reason to do it: a breakthrough in medicine would bring more investment and a far better reputation. The point is that today they can't, because of concrete limits that come from the very nature of those fields.

An intelligence different from ours

The natural intuition is that an AI able to solve problems that have been open for decades in maths should do equally well elsewhere. That step is anything but automatic.

The first thing to internalise is that the intelligence of these systems is profoundly different from ours, and that we need to let go, however hard it is, of the assumptions we carry over from human intelligence. A model can be extremely strong in one field and fail miserably at a task that seems trivial to us. In humans, abilities are far more even across domains.

To understand why maths sits on one side of this gap, you need to look at where a good part of the recent progress comes from: reinforcement learning.

Reinforcement learning and RLVR

It's true that LLMs are trained to predict the next token, but that's half the story. That phase is called pre-training: the model processes huge amounts of text of every kind and learns to predict what comes next.

Then there's post-training, which matters more and more, and reinforcement learning is part of it. Here the goal changes: it's no longer about predicting, but about reaching the right answer. The model proposes a solution, the solution is evaluated, and the model is rewarded or not.

In one specific variant, RLVR (reinforcement learning from verifiable rewards), the evaluation is automatic. It needs two ingredients: large numbers of problems of the same kind, and a way to check automatically whether the answer is correct. The key word is verifiability.

The real-world limit: why not medicine

This tells you where to expect progress: in every discipline where an answer can be checked by computation. An everyday example is structured data. Today an LLM returns structured output with very high precision, if you ask for it: the structure is verifiable, and AI companies very likely have reinforcement learning environments dedicated to exactly that.

The flip side is that problems that require interaction with the outside world are far harder to crack. A new drug or a new therapy needs more than reasoning and computational checks: it needs real experiments. There, progress will be slower and more limited, at least for now. The limit is clear to everyone, and several teams are working on it from different angles.

Maths is the perfect case: with a proof assistant like Lean, a proof can be checked entirely by computation, without touching the outside world. And it's the same principle that explains the third story.

3. AI has learned to remake software (and video games)

Photoshop rebuilt in a week: the ArtCraft apps

Between 30 September and 7 October the ArtCraft team published a whole family of free, open source applications on GitHub:

PhotoCraft for Photoshop, VectorCraft for Illustrator, FilmCraft for Premiere, LightCraft for Lightroom, EffectCraft for After Effects, DesignCraft for InDesign, plus an Acrobat clone;
WordCraft, GridCraft and DeckCraft for Word, Excel and PowerPoint;
CADCraft for AutoCAD and SoundCraft for Pro Tools.

Behind it there's no big tech company, but a developer, Brandon Thomas, with a very small team. He used Claude Opus 5.5 and wrote everything in Rust, with a WebAssembly version that runs in the browser. Claude appears as co-author on most commits. The response was enthusiastic: PhotoCraft passed 20,000 stars on GitHub in about a week.

Why Adobe

By his own account, the last straw for Thomas was the cancellation fee. It's a hot topic: in 2024 the US government sued Adobe over exactly those fees and the difficulty of cancelling a subscription, and the case was settled for 150 million dollars. Adobe denies any wrongdoing.

How to clone software without its code

According to the team, the vendors' code was never touched. The README describes an implementation based solely on public specifications and observed behaviour. It's black box reverse engineering:

the agents study documentation, file formats, screenshots and tutorials;
they break the program into components (layers, brushes, filters);
they generate code for each piece;
they compare the output with that of the real Photoshop, and start again if it doesn't match.

For PSD files there's a specification published by Adobe, the same route taken by Photopea or Pixelmator. CADCraft is trickier, because the DWG format has no open specification: the team uses a third-party library, acadrust (MPL-2.0 licence), and states in black and white that it has no connection with Autodesk.

AI-driven decompilers

AI decompilers do exist, though. Projects like GhidraMCP or Reverse Engineer Anything connect agents to Ghidra, IDA or Hopper, and the agent can inspect a compiled app and rebuild it. For ArtCraft, so far, nobody has shown evidence that vendor code was used.

How well do they actually work

They're alpha releases, and the team says so openly. According to the roadmap, PhotoCraft today covers 25-35% of what a professional needs for everyday work, and people who've tried it report bugs and unpredictable tools. Thomas promises feature parity within a month: a decidedly optimistic goal.

Why AI is so good at it

Reverse engineering has been around for forty years. What changed now?

It's the maths argument, applied to software. Reverse engineering is a verifiable problem par excellence: you produce a hypothesis, compile it, run it and compare it with the original. Either it matches, or it doesn't. The same trial-and-check loop, but automated and running in parallel across hundreds of functions.

A serious clean room used to require two separate teams, lawyers and months or years of work. Today that cost has collapsed by orders of magnitude.

Video games remade and mixed together

The same wave has hit video games, starting at the end of September. The first viral case was Chasm's project on 19 September: Skate 3 rewritten in Rust, then the skating physics dropped into Call of Duty: Modern Warfare 2. From there it exploded: Mario in Elden Ring, Spider-Man swinging through Gotham, Mario Kart in Call of Duty Zombies, Minecraft inside Elden Ring.

There are two techniques:

overlay: the two games run at the same time and the characters of one are overlaid on the other, a kind of advanced green screen but with linked inputs. You draw a bow in Minecraft, and Steve draws a bow in Elden Ring;
decompile and rebuild: the games are decompiled and rebuilt in a modern engine, like Bevy in Rust, stitching together systems that were never meant to be compatible, such as skeletons and animations.

AI carries a lot of weight, but on top of an enormous amount of human work. Chasm describes the project as almost entirely vibe-coded, but it relies on years of hand-made reverse engineering by others, and the Minecraft part took weeks of manual tuning.

Decompilations and games ported to PC

Beyond the mashups there's the whole decompilation and PC-port scene:

the decompilation of Super Smash Bros. Melee reached 100% on 7 September, after more than six years, with AI speeding up the final stretch;
the Snowboard Kids one went from almost two years of work to 84 days;
Fable 2 was made to run on PC in about an hour;
one developer burned through over 500 billion tokens in three months to decompile an entire FPS into C++.

Verifiability matters here too, fully. In matching decompilation the compiler either produces a binary byte for byte identical to the original, or it doesn't. Wrong answers discard themselves.

How modders reacted

Not everyone applauded. The N64 Recomp Discord neither shows nor supports vibe-coded projects, some ports deliberately present themselves as "100% written by humans", and some veteran modders threaten to quit if this becomes the norm.

But is it legal?

It depends on what you use as input. Copyright protects code as it's written, not what the code does.

In Europe the Court of Justice said so clearly in 2012, in SAS Institute v World Programming: functionality, programming language and file formats are not protected. The Software Directive, in Article 5(3), grants the right to observe, study and test a program, and contractual clauses that forbid it are void.

On decompilation the margin is narrower: Article 6 allows it only for interoperability, only for the necessary parts, and never to build a substantially similar program. In the United States there are favourable precedents, Sega v Accolade (1992) and Google v Oracle (2021), but courts have also enforced anti reverse engineering clauses against people who accepted the licence.

AI adds a new problem. The classic clean room works because you prove that whoever wrote the code never saw the original. But a model trained on half the internet may have seen it in its training data. The textbook case is the Claude Code source leak of 31 March: within days, AI-made "clean room" reimplementations appeared, and whether they really count as such is still an open question. There's a flip side too: in the United States a work generated entirely by AI can't be protected, so the clone itself might end up without copyright.

Licences and patents: are vendors defenceless?

Licences try to shut the door. Adobe's terms of use, in section 17, treat even monitoring an app's inputs and outputs in order to recreate it as reverse engineering. Microsoft forbids using its products to replicate their functionality, and Autodesk forbids reverse engineering and decompilation except where the law allows it. The limit is that a contract only binds whoever accepted it: if a team works from public documents and behaviour described by others, it isn't clear what the vendor can do to them.

They're not defenceless, though. There are patents, which cover a method however the code is written, and Adobe holds thousands on software features. There are trademarks. These are slow, public routes, but they exist. And there's look and feel: PhotoCraft's README introduces itself by saying that if you know Photoshop, you already know PhotoCraft, and that's where the risk is most concrete.

For games the picture is even less favourable: publishers have historically been aggressive. Take-Two hit the re3 GTA project with a DMCA notice in 2021, later settled in 2023. The video of Super Mario 64 inside Elden Ring has already been taken down after a copyright claim. And many mashups use original assets, which is the most slippery ground of all.

What changes for software vendors

Code stops being the moat. If an app's visible behaviour can be rebuilt in a week, value shifts to what isn't code: years of files in proprietary formats, cloud services behind an account, plugin ecosystems, identity management, certifications, support. None of the ArtCraft apps run Photoshop plugins or VBA macros.

The most exposed are those who live mainly off a desktop app with a documented format: Adobe's apps and Autodesk's drawing tools are the most at risk. Microsoft 365 less so, because it's also email, Teams, SharePoint and identity: you can rebuild the editor, but the platform stays.

And for software buyers

For companies that buy licences, the main novelty is negotiating leverage. Even without migrating, an alternative tested on a group of light users changes the conversation at renewal time.

With a few precautions:

fake installers with famous names, the classic malware vehicle when a project goes viral;
no IP indemnity and no support;
the risk of paying twice, adopting the clone while renewing the licences anyway.

And for those of us who build custom software, there are two sides. On one hand, you can now rebuild or modernise a legacy system without its source code in timeframes that were unthinkable until yesterday. On the other, your own product becomes replicable too: if the value you sell is only the interface, someone can rebuild it just by watching it run.

The common thread: where the answer can be checked, AI gets there

Three stories, one mechanism. AI isn't uniformly intelligent: it's extraordinarily strong wherever there's an automatic way to say "right" or "wrong". Maths with Lean, an app's output compared with the original's, a binary that recompiles identical. Where verification goes through the real world, as in medicine, progress is much slower.

For people who build software there are three practical consequences.

Ask how verifiable what you're building is. The more a task has an automatic success criterion, the sooner AI will be able to do it. That applies to product features and to internal processes: tests, format conversions and code migrations are where AI already delivers the most today.

Move value beyond the interface. If watching software run is enough to rebuild it, the defence is data, integrations, service and trust. Code can be copied, trust can't.

Don't mistake the result for understanding. It holds for mathematicians and it holds for generated code: a solution nobody can explain works until something changes. That's where human work is moving: understanding, and choosing the next question.

Frequently asked questions

What did OpenAI publish on 6 October 2026? A GitHub repository with hundreds of maths papers containing solutions, or significant partial advances, for around 370 families of results. About 40% come with a Lean proof attached. They were produced by an internal, unreleased model, the same one used for Navier-Stokes.

What is Lean and why does it matter? Lean is a proof assistant: a formal language for writing mathematical proofs that a program checks automatically. If a Lean proof passes the check it's correct, with no need to trust whoever wrote it.

How much compute did OpenAI's maths results take? Around 3 hours per problem on average, for the vast majority of results. Of around 4,000 problems submitted, a significant share but far from all were solved, and three results without a Lean certificate have already been withdrawn because of errors.

Does AI only solve maths problems by finding counterexamples? No. Even when the solution is a counterexample, the path to finding it is rarely trivial, and many of the results published by OpenAI are complex constructions that mathematicians find counter-intuitive.

Why is AI so good at maths? Because of reinforcement learning, and in particular RLVR (reinforcement learning from verifiable rewards): the model is rewarded when it reaches the correct answer, and in maths correctness can be checked automatically. The more verifiable a domain is, the faster AI improves at it.

Why isn't AI making as much progress in medicine? Because in medicine final verification goes through real experiments, not computation. Without fast, automatic verification, reinforcement learning has much less room to work, at least for now.

What are the ArtCraft apps? Free, open source clones of Photoshop, Illustrator, Premiere, Lightroom, After Effects, InDesign, Acrobat, Word, Excel, PowerPoint, AutoCAD and Pro Tools, published on GitHub between 30 September and 7 October 2026. They were built by Brandon Thomas with a small team, using Claude Opus 5.5 and Rust. They're still in alpha.

How do you clone software without its source code? With black box reverse engineering: you study the app's documentation, file formats and behaviour, break it into components, generate code for each one and compare the output with the original's until they match.

Is it legal to clone software with AI? It depends on the input. Copyright protects code, not functionality: in Europe the 2012 SAS Institute ruling and the Software Directive allow you to observe, study and test a program. Decompilation is only allowed for interoperability. Patents, trademarks, look and feel and licence clauses for those who accepted them still apply.

What are AI-made video game mashups? Projects that combine different games, such as Minecraft in Elden Ring or Skate 3's physics in Call of Duty, either by overlaying two running games with linked inputs or by decompiling them and rebuilding them in a modern engine.

What changes for companies that sell or buy software? For vendors, code is no longer a defence: value shifts to data, integrations, cloud services, ecosystems and support. For buyers, an open source alternative, even an immature one, becomes leverage at renewal, with the risks of fake installers, no indemnity and licences paid twice.