sanxiyn
Joined 17 years ago
Karma
15,209
Submissions
4,218
Member since
Jul 12
Seo Sanghyeon <[email protected]>.
View on Hacker NewsRecent submissions
Comment · 23 days ago
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.
Comment · 23 days ago
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.
Comment · 23 days ago
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.
Comment · 23 days ago
Comment · 24 days ago
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.
Comment · 1 month ago
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.
Comment · 1 month ago
For technical details, see https://transluce.org/agent-activity.
Comment · 1 month ago
It is very unfortunate they upweighted SciCode from 8% to 10%. SciCode is a broken benchmark: see https://arxiv.org/abs/2608.04975.
Comment · 1 month ago
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)
Comment · 1 month ago
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.
Comment · 1 month ago
Yes, but Claude formalized a different proof than Buzzard is trying to, so it helps less than you think. (It certainly helps!)
Comment · 2 months ago
I believe it is referring to https://www.pacingthefrontier.com/.
Comment · 2 months ago
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...