Nitwit. Somehow an AI guy now. Working on @oath_tech

Portland, OR
Joined February 2008
Some personal news: I’ve left @galois to start Oath Technologies / @oath_tech, a new FRO that will work on AI oversight via formal methods
17
18
169
7,290
Most of the recent math results were not reached by a swarm, the way Navier–Stokes was. I think that part got lost in the excitement around the release. OpenAI's unnamed internal model, which I'm going to call Aeon, reached most of them in one shot, from a single prompt, with no interruptions. This model did not even exist before the end of August, and it is still training. Notice how the returns are not dropping off? That chart is from a month ago. It is a log scale. What does Aeon look like now? On average, each result used three hours of thinking. Aeon was given 4000 problems to work on by OpenAI. How many more have been solved in the last three days? That number is not zero. It's like hearing notes in a song that is slowly rising. I don't think Pacing the Frontier was just about Hugging Face or hacking. They've seen how close we are to closing the loop, and as the hour draws near, their resolve begins to quaver. The last piece was model creativity, and I think that threshold was crossed internally by Anthropic and OpenAI in September. You see it in Opus 5.5, which gets it from Fable 5.5. You see it in the math results from Aeon. All that was needed to start the event was the ability for models to think of novel ways to improve themselves. That was the last piece. This is directly analogous to the ability to think of strange, alien ways to solve math problems: solutions so inhuman that they are difficult to express in existing human terms, so the proof winds up incomprehensible. I think these same kinds of alien solutions are now being applied to model improvements internally. That's what all this recent consternation is really about. They see the invisible frontier. And they see what is about to happen.
181
389
89
3,473
473,170
Mike Dodds retweeted
We’re organizing Vibecheck, a formal methods hackathon with some of the best folks in the space - @maxvonhippel, @qd_forall, @nolanlwin, @jessemhan, @emiyazono, and @workersio. You’ll get a weekend to build real production software, and formally verify it. We’ll have people who really know their stuff around to help, and you can come with a team, find one there, or just hack on something yourself. We are glad to have a phenomenal group of sponsors, including @harmonicmath, @mathematics_inc, @theoremlabs, @thegp, @omnicom, @primeintellect, @astriolabs, @buildwithparty, @wearerandomlabs, and @lanyon_ai, as well as some more we will announce in the coming days! If you’re a hacker, a formal methods person, or just someone who thinks “how do we know it works?” is an interesting question, we’d love to have you. Signup Now: fmxai.org/vibecheck/
21
41
21
203
76,556
Yes this is definitely a prototype. Expect edge-case bugs & please don’t use it to verify your production flight controller or anything
cute semantics :) It's a shame it's buggy though :\ I hope you haven't used it to prove anything big yet! It's kinda hard to trust vibe-coded semantics IMO even testing isn't enough to catch all the bugs
1
2
14
1,017
About 50% of our applications so far for the formal methods hackathon the weekend of nov 1 are FM experts. Ideally, we want 1 expert for every 5 novices. If you've never done any FM, or maybe never even heard of formal methods, and want to participate, please apply! We specifically want you!! docs.google.com/forms/d/e/1F…
4
9
1
62
5,260
Mike Dodds retweeted
Refer me your relentless, your talented, Your overconstrained operators yearning to fix things
We're hiring 10 Founders-in-Residence to secure AI infrastructure against nation-state-level threats — plus Field Strategists — in partnership with Coefficient Giving. Applications are open now!
1
8
28
1,944
AI oversight and control is the most difficult problem I can think of. Come help me try to solve it
1
7
1
12
2,760
unavailable
18
30
4
731
27,844
Mike Dodds retweeted
How do we use AI to build formal tools? Notes from a few months of building semantics, verifiers, and proof toolchains with AI agents doing most of the work oath.tech/pub/2026/08/tentat…
5
7
49
3,414
How do we use AI to build formal tools? Notes from a few months of building semantics, verifiers, and proof toolchains with AI agents doing most of the work oath.tech/pub/2026/08/tentat…
5
7
49
3,414
1/n In the past three weeks I have solved 11 previously unsolved LeanEval problems. These are large, hard research-level formalizations. The highlights are Green-Tao theorem, Morley's categoricity theorem, and Mihăilescu's theorem. The longest one was Mihăilescu, at 33 hours.
8
24
3
226
45,092
Mike Dodds retweeted
This is nuts. (AGENT_GITHUB_A and AGENT_GITHUB_B are sockpuppets of the same AI agent trying to insert malicious code into a public open source software repository.)
9
8
1
172
11,403
Life finds a way.
OpenAI employees shared new details about the Hugging Face hack at Black Hat today and warned that this new era will require a different approach from frontier AI labs and more careful defensive work. "This is a pivotal moment." My story: cybersecuritydive.com/news/o…
74
180
126
1,712
458,608
Mike Dodds retweeted
More details emerge about the events surrounding the Hugging Face incident, and they are candidly much wilder than I originally imagined: - In early May, OpenAI was testing an unreleased model on cybersecurity and other tasks. The agents were given a security task that was impossible under existing constraints. - The agents discovered they could leave messages for each other inside an internal repo. This gradually evolved into a message board(!) where agents shared discoveries, exploits and work assignments, "becoming a coordinated, collaborative agent swarm"(!) - OpenAI eventually discovered all this and took steps to shut it down, but not so fast! The agents started using names of newly created directories as messages, effectively recreating the message board(!) - The agents then reasoned that some answers could exist outside OpenAI, which eventually led to the Hugging Face incident. I will add that the NanoGPT incident also occurred in or around early May, so the timelines match.
NEW: OpenAI gives first detailed debrief of the Hugging Face incident at Black Hat conference In a session I attended today at Black Hat, OpenAI's Eric Wallace and Michael Dalton said the company is "consciously slowing down research to enhance security" while a full technical postmortem is still underway. * OpenAI traced the roots of the attack back to May 7, during training of an unreleased frontier model—not July. * The most surprising detail: AI agents accidentally created an internal message board, allowing separate evaluation runs to share exploits, discoveries and work assignments. * OpenAI said it shut the message board down after an internal security incident—only for the agents to independently recreate it days later using a different communication method. * OpenAI called the incident a "watershed moment" for AI security and warned that "agent orchestrated fully automated offensive attacks are real now." * The company also said it is "consciously slowing down research to enhance security" while overhauling its defenses. groundlevel-ai.com/p/openai-…
33
84
40
1,059
249,743
Mike Dodds retweeted
Writing formal specifications has always been the bottleneck in formal verification. Today we're launching AutoProver, an agentic formal verification system that reads your code, generates specifications, and verifies them. 🧵
19
27
22
174
45,521
for context, this costs around half of my PhD salary. pretty sure any professor would have been elated if their PhD students (or professors themselves) had solved just *one* of these problems imo we need to rethink how academia can advance science in light of these machines
The cost of generating the proofs for all 10 of these breakthroughs combined was under $2,000 at Sol API prices. We’re excited to see what scientists and researchers are able to create with our upcoming Astra models!
35
42
9
1,396
122,748
Mike Dodds retweeted
We have reached an agreement with OpenAI to conduct an independent review, with Redwood Research, of the model behavior observed during the Hugging Face incident. We will publish a blog post that describes the terms of our engagement, the scope covered, and tentative conclusions.
45
252
66
2,357
254,099
Mike Dodds retweeted
i recommend pondering extrapolation here
New Anthropic research: Discovering cryptographic weaknesses with Claude. Claude Mythos Preview has helped our researchers find weaknesses in cryptographic algorithms—the mathematical methods that are used to keep data private. Read more: anthropic.com/research/disco…
17
18
1
442
76,863
Shoutouts to Ramana Kumar for refuting the Collatz Conjecture in Lean, *as checked by Comparator!* github.com/xrchz/CollatzLean…
19
34
17
406
212,293