Hacker News: qbit42

New comment by qbit42 in "Simons Foundation launches $15M effort to help mathematicians navigate AI era"

qbit42 — Thu, 15 Oct 2026 19:40:26 +0000

For what it's worth, most mathematicians are paid to teach, and the amount of research funding going into mathematics is relatively small. Plus, there are rare but important broader advancements due to pure and applied math that are hard to predict in advance (e.g., cryptography, compressed sensing).

Mathematicians also decide what to prove in their research - taste is not a skill we have RLVR'd away (yet, not claiming this is fundamental).

Of course, the field is being fundamentally transformed, it will probably end up looking more like experimental science in the future.

New comment by qbit42 in "Simons Foundation launches $15M effort to help mathematicians navigate AI era"

qbit42 — Thu, 15 Oct 2026 19:32:10 +0000

In his recent interviews, he says he has very little time to do math these days outside of research meetings with his PhD students and postdocs.

New comment by qbit42 in "Neural networks are clean"

qbit42 — Thu, 15 Oct 2026 19:30:45 +0000

Is the use of "generalization" like this standard in mech interpretability? Seems undesirable given the typical definition in ML.

New comment by qbit42 in "If math is more than proof, we need to better celebrate the rest of it"

qbit42 — Sat, 19 Sep 2026 11:58:56 +0000

It just looked to me like the GP hadn't read the article and assumed it was a post by Tao. You are right about Tao of course, no objections there.

New comment by qbit42 in "If math is more than proof, we need to better celebrate the rest of it"

qbit42 — Sat, 19 Sep 2026 11:42:28 +0000

This post isn't by Tao.

New comment by qbit42 in "Artificial intelligence now beats some of the best human forecasters"

qbit42 — Thu, 17 Sep 2026 17:28:33 +0000

The quant firms are heavy AI investors I believe.

New comment by qbit42 in "After Math"

qbit42 — Sun, 13 Sep 2026 11:20:24 +0000

You can also brute force the existence of a proof...

It is true that the biggest splashes have been from counterexamples and such, but I have seen many smaller examples of proving positive results in my own field.

Perhaps not superhuman yet but sufficient to completely upend the status quo. And I'm supposed to believe that this won't change in a year? or two?

New comment by qbit42 in "After Math"

qbit42 — Sun, 13 Sep 2026 11:16:16 +0000

Maybe, but what remains of the human professional mathematics will be unrecognizable (at least for those without tenure I guess). All of our credit assignment systems are breaking and access to computational/financial resources is becoming way more important. Math has been one of the most open academic fields but everyone is becoming afraid of sharing their ideas. Personally, my job has slowly been moving from open-ended brainstorming to prompting/digesting LLM output (or LLM output transmitted by grad students). And the students are so demoralized! Also, the academic funding structures which have supported math departments are looking less and less stable - I imagine many of them will shrink.

New comment by qbit42 in "ChatGPT Images 2.5"

qbit42 — Wed, 09 Sep 2026 08:35:39 +0000

And getting paid…

New comment by qbit42 in "On the Navier–Stokes Millennium Prize Problem"

qbit42 — Tue, 08 Sep 2026 18:15:26 +0000

I heard Hodge conjecture? Third-hand rumor though...

New comment by qbit42 in "Formalizing Fermat's Last Theorem"

qbit42 — Sun, 06 Sep 2026 07:48:56 +0000

It's not impossible, but I also know of no instances of an AI being told to prove something in Lean and exploiting such tricks. Surely Anthropic also had some agents looking for issues with the generated proofs. Personally, I am also comfortable trusting Kevin Buzzard, who was leading the human team aiming to formalize FLT and discussed this a bit on his blog.

Finally, the good thing about Lean is that if anyone ever finds a new compiler bug (which, by the way, are being searched for extensively using AI), you can correct the bug and recompile any old proofs of which you are suspicious. Any tricks in a false proof must be exploiting a bug in the Lean compiler, so as we increase trust in the compiler over time we also increase trust in every previously compiled proof.

I agree it's not a 100% guarantee, but in this case the human proof is well-understood and written about by many experts, so I think Claude had plenty of material to work with. Even if the task was enormous, I don't think any of the individual steps are out of the scope of what we have seen from current AI tools.

New comment by qbit42 in "Fermat's Last Theorem in Lean 4"

qbit42 — Sat, 05 Sep 2026 18:05:04 +0000

I have never seen an AI or a human produce a false proof without explicitly using weird meta programming tricks that are very suspicious. No "good faith" Lean proofs have every been shown faulty, to the best of my knowledge. While the risk is non-zero, many of the AI companies are also trying to find bugs in the Lean kernel, so it is becoming very well stress-tested.

New comment by qbit42 in "Formalizing Fermat's Last Theorem"

qbit42 — Sat, 05 Sep 2026 10:55:30 +0000

You just have to trust the statement and the lean compiler, not the proof. The compiler certainly still has remaining bugs, but I have never seen a bug leading to a false proof in good faith, only via obscure meta programming tricks. The nice thing is that the multiple versions of the compiler are constantly being stress tested. Still, there is plenty of work that could be done to make the compiler more trustworthy / easier to verify.

New comment by qbit42 in "Claude Fable 5.1 and Claude Mythos 5.1"

qbit42 — Wed, 02 Sep 2026 06:29:52 +0000

Watermarking just alters the pseudorandom number generator. If "I like turtles" was previously the response to your prompt with probability 100%, it will still be so. This is why watermarking is only effective for long strings of text

New comment by qbit42 in "AnkiDroid: Google Play no longer allowing Open Collective donation link"

qbit42 — Tue, 01 Sep 2026 13:04:45 +0000

I think the old reddit redirect extension gets around this somehow, that has worked for me lately (occasionally with some toggling of the extension). Although maybe it's best to just use less reddit tbh

New comment by qbit42 in "Abdominal fat predicts heart disease risk better than BMI"

qbit42 — Sun, 16 Aug 2026 03:01:30 +0000

Are legumes not "real food"?

New comment by qbit42 in "Europe's scorched landscapes seen from space after summer heatwaves"

qbit42 — Sun, 16 Aug 2026 02:58:13 +0000

I somewhat agree, and I have not stopped eating beef entirely. I think that forbidding is overkill but agree that lots of related subsidies should be eliminated (honestly, if meat were just priced w/o current subsidies, we'd be in far better shape).

But you have to have some public consensus or the government will never implement such changes due to their unpopularity. This is why I think promoting some reduction in individual meat consumption is still valuable - it is good for average people to reflect on their consumption or they will vote out anyone who attempts to change it.

I don't think that the focus should be on individual blame (even just for the reason that this is politically nonviable). But you at least need to amass some collective awareness.

New comment by qbit42 in "Europe's scorched landscapes seen from space after summer heatwaves"

qbit42 — Sat, 15 Aug 2026 20:13:30 +0000

I mean, it's a collective action problem. Individual consumption of normal people is a huge contributor to global energy demands / pollution / etc. You don't have to change your behavior but if no one does in the coming decades then we're pretty fucked.

Not to let the 1% off the hook. Por que no los dos

New comment by qbit42 in "Principia Mathematica is modern and insightful"

qbit42 — Thu, 13 Aug 2026 07:44:29 +0000

There is not a single foundation - you can choose. The differences are rarely important for working mathematicians though. Most know enough of ZFC to get by and ignore foundations tbh

New comment by qbit42 in "What happens if an entire class of workers loses faith in their careers"

qbit42 — Fri, 07 Aug 2026 13:58:39 +0000

People talk on the phone all the time on every US metro I’ve tried. Seems fine if they’re not on speaker or raising their voice