sanxiyn

I am not sure what you are trying to imply, but quasi-Riemann hypothesis is in fact not Riemann hypothesis and resolution of the former, while truly fucking amazing (it wouldn't be an exaggeration to say it is a discovery of century), gives no hint how to resolve the later.

As I said, a proper eval is better, but it measures something real that gives a good training signal, and there is lack of good alternatives for math eval. Since the result is 372/4000, it is also unsaturated.

OpenAI in fact didn't know what to do with results and didn't want to flood the world, so they asked mathematicians. Mathematicians recommended OpenAI to release them. My guess is it would have been better for OpenAI if they didn't release them. OpenAI is basically doing this as a goodwill.

(See https://agmai.org/general-sep29/ for the recommendation in question.)

People seem to have very misguided ideas about why OpenAI is doing this at all. It is not to brag or to torture mathematicians. It is an eval. OpenAI is known to be willing to pay large amount of money to get a good eval, think FrontierMath. FrontierMath is now saturated, so they need a replacement eval for math. Open math problems are actually a fairly good eval, although a proper eval is better (eg FrontierMath has known difficulty and have tiers from 1 to 4).

Mathematicians would prefer if OpenAI didn't use open math problems as an eval, but OpenAI is not obliged. I actually think OpenAI wouldn't point AI to open math problems if unsaturated FrontierMath Super Duper is available, as it just angers mathematicians, but such eval is not in fact available. Given OpenAI used open math problems as an eval, they could just throw out the result (this is in fact better as an eval since it will keep problems useful longer), but mathematicians preferred to see the result. So OpenAI released them.

Yes: https://x.com/ElliotGlazer/status/2108026240582246600

This is basically On proof and progress in mathematics by Thurston restated. When Thurston wrote it in 1994, many people didn't understand what he is talking about.

https://arxiv.org/abs/math/9404236

This in fact already happened (exactly OpenClaw, even).

AI assistant hacks gym website in first known Australian autonomous cyber attack: https://www.abc.net.au/news/2026-08-10/ai-assistant-hacks-gy...

General opinion at the time was it was in fact ambiguous who was legally liable.

For technical details, see https://transluce.org/agent-activity.

It is very unfortunate they upweighted SciCode from 8% to 10%. SciCode is a broken benchmark: see https://arxiv.org/abs/2608.04975.

Lean's three standard axioms are documented in The Lean Language Reference.

https://lean-lang.org/doc/reference/latest/Axioms/#standard-...

The axiom of choice: axiom Classical.choice {α : Sort u} : Nonempty α → α

The axiom of propositional extensionality: axiom propext {a b : Prop} : (a ↔ b) → a = b

The quotient axiom: axiom Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Eq (Quot.mk r a) (Quot.mk r b)

New proof: The Classification of the Finite Simple Groups (American Mathematical Society Mathematical Surveys and Monographs vol. 40).

https://www.ams.org/publications/authors/books/postpub/surv-...

Number 1 (1994), Number 2 (1995), Number 3 (1997), Number 4 (1999), Number 5 (2002), Number 6 (2004), Number 7 (2018), Number 8 (2018), Number 9 (2021), Number 10 (2023). 10 volumes and >4000 pages so far, number 11 is in progress, and end is in sight, probably two more volumes or so.

https://www.ams.org/journals/notices/201806/rnoti-p646.pdf

People were curious what is going on during 2004-2018. A progress report was published in 2018 right before publication of number 7 and 8. In a sense it was the peak, number 8 completes the proof of so-called "generic case". The rest is "special case". It doesn't mean things get easier, but in some specific sense number 8 completed proof for almost all groups.

Now new proof's end is in sight, people are planning new new proof.

Yes, but Claude formalized a different proof than Buzzard is trying to, so it helps less than you think. (It certainly helps!)

I believe it is referring to https://www.pacingthefrontier.com/.

The consensus is that proof is in fact incorrect. People tried really hard (like putting in a year of effort) and most converged to the same place, that proof of 3.12 is incorrect or has a gap. Peter Scholze (who won Fields Medal) and Jakob Stix did a writeup. People seem to think Shinichi Mochizuki correctly reduced ABC conjecture to 3.12, but didn't prove 3.12, and also are doubtful about the whole program because 3.12 doesn't seem any easier than ABC conjecture while complicating everything.

https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...

People go through trouble to write Python-shaped DSL for GPU compute. We will go "why o why?", but apparently such things are necessary to succeed in the market.

I think volume is itself good and help Stripe negotiate lower rate with banks etc.

Congratulations to the first NetBSD release with RISC-V port!

This is not okay. NSA should audit both OpenAI and Anthropic on national security ground. This seems far more justifiable than Mythos export control.

Yes, I agree it is effectively a blanket ban (above some capability) for now. I hope AI alignment research advances in the future so that it is not so.

I think we agree on all specifics now and just fighting for terminology. Thanks for the discussion!

That is a difficult question I am not qualified to answer, but Mythos 5 was export controlled for a brief time due to its cybersecurity capability and implications to national security, so for cybersecurity "as capable as Mythos 5" seems to be a good baseline. I wouldn't know for biosecurity though.

UK AISI preliminary evaluation suggests Kimi K3 is not capable enough for cybersecurity in this sense.

https://www.aisi.gov.uk/blog/preliminary-assessment-of-kimi-...

Agreed, and that serves Anthropic. It seems unproblematic to me. Dario probably sincerely believes in mandatory safety testing for capable models (open and closed), and likes the fact that it aligns with Anthropic's interest.

De facto ban on capable open-weight models doesn't seem inconsistent with Dario's statement to me. One, it is de facto, not de jure, and it can and will change as AI alignment research advances. Two, it is only capable open-weight models, not open-weight models. In fact, Dario says non-dangerous (which for now is mostly non-capable) open-weight models are a public good, and I agree.

Yes, I agree that Anthropic is advocating a ban on capable open-weight models until reasonable AI alignment research advance happens in the future. In return, I hope you agree with me that Anthropic has never advocated for a ban on open-weight models.

I think Gemma will be fine. Most open-weight models are not capable enough to be dangerous. Yes, I can't think of any capable open-weight model that would survive reasonable safety testing.

I know, but "we don't know how to make it not dangerous, so it should be allowed to release dangerous things" is... not convincing?

Any reasonable safety testing should include finetuning and safety margin to account for others may do better finetuning.

I agree we don't know how capable open-weight models could possibly pass any reasonable safety testing NOW, but that's about currently abysmal state of AI alignment research, not about what is possible in principle. I don't see any internal inconsistency, to be honest. Since Anthropic does not release any capable open-weight models, it's not their problem. If mandatory safety testing is established, companies who want to release capable open-weight models will work on AI alignment research so that they can pass. This seems to be a good outcome to me.

For what? Would authors and publishers like that?

No, this is not the case for human security researchers and I don't see why it should be true for LLMs.

If a model fails the test, it should be banned. He is not advocating a ban of open-weight models. He is advocating a ban of models that fail mandatory safety testing. Seems reasonable and straightforward.