Human mathematicians are being outcounterexampled • Hacker News Board

Re: Human mathematicians are being outcounterexampled

#211

Post by jebarker » Tue, Jul 21, 2026, 3:08 PM UTC

voxic11 wrote: post #184

randusername wrote: post #181

Earlier quoted context omitted.

I thought there was a lot of buzz about AI creativity after the infamous move 37 in that series?

Yes but it was so shocking because it was such an inhuman, "unaesthetic" play. It was considered to be "creative" in that no human would have thought of making the move, so it can't simply be copying human play.

Indeed. To get "aesthetic" play you would have to mimic real human play for an interesting reason: the space of possible Go configurations and games is so mind-bogglingly vast that all of human history has only ever seen a infinitesimal sample. So any sense of aesthetics is just a consequence of chance and memetics. AlphaZero is effectively exploring a new branch of Go history so its aesthetics are completely different. Although maybe that just shows that the idea of aesthetics here isn't very meaningful.

Re: Human mathematicians are being outcounterexampled

#212

Post by elias_t » Tue, Jul 21, 2026, 3:10 PM UTC

hiddencost wrote: post #173

elias_t wrote: post #139

I wonder if at some point mathematicians will be over-flooded with proofs to check and eventually some over confident false claim will make it into math. Maybe in the future the work of Mathematicians will be like the ones of SWEs with AI, check thousands of lines of AI generated proof and find the subtle errors

That's why the author refused to read a proof from someone he knew until it was formalized in Lean.

Yes it compresses the proofs but still "Sol had generated 1.2 million lines of Lean code in the three weeks that it had worked on the project". I mean how do you even verify that?

Re: Human mathematicians are being outcounterexampled

#213

Post by elias_t » Tue, Jul 21, 2026, 3:11 PM UTC

inigyou wrote: post #167

ykonstant wrote: post #145

Earlier quoted context omitted.

>I wonder if at some point mathematicians will be over-flooded with proofs to check and eventually some over confident false claim will make it into math. That point had come some time ago. Nowadays the literature is both enormous and littered with false proofs and an unknown, but nonzero, number of false published results.

There are projects to take the entirety of humanity's mathematical knowledge and pour it into a proof checker.

Do you have the names of such projects?

Re: Human mathematicians are being outcounterexampled

#214

Post by dTal » Tue, Jul 21, 2026, 3:11 PM UTC

Diogenesian wrote: post #203

noslenwerdna wrote: post #198

Earlier quoted context omitted.

This is a very close minded definition of evil. What is the threshold of environmental impact before something is evil and its use indefensible? What level of copyright violation will send us to hell?

I didn't give a definition of evil, so "close-minded definition" is just a dishonest way of expressing that you subjectively disagree with me. Likewise with trying to make me judge an objective threshold for pollution. It really should be that any polluter needs to morally justify their actions. I find "mostly illusory productivity improvements in white-collar employment" to be an especially indefensible reason for f…

Thank you for using the phrase "stochastic parrot". I only request that you use it at the beginning of your long comments, rather than the end. It saves time.

Re: Human mathematicians are being outcounterexampled

#215

Post by Jweb_Guru » Tue, Jul 21, 2026, 3:16 PM UTC

elias_t wrote: post #212

hiddencost wrote: post #173

Earlier quoted context omitted.

That's why the author refused to read a proof from someone he knew until it was formalized in Lean.

Yes it compresses the proofs but still "Sol had generated 1.2 million lines of Lean code in the three weeks that it had worked on the project". I mean how do you even verify that?

Because you literally don't have to actually understand the proofs, just the definitions and proposition chain. Most of the code is going to be proving auxiliary lemmas or building up internal definitions that aren't needed to understand the final proposition. Then all you have to do is make sure the proof doesn't use any axioms and you're good. Being able to confidently do this is why proof assistants like Lean are really not just another programming language.

(That's not to say there's no value to making the proof themselves nicer--compilation time and reusability can actually be a really big deal in formalized mathematics!--but it's way less important than it is in software).

Re: Human mathematicians are being outcounterexampled

#216

Post by datsci_est_2015 » Tue, Jul 21, 2026, 3:18 PM UTC

vonneumannstan wrote: post #207

tantalor wrote: post #176

Earlier quoted context omitted.

That's not why. It's because counterexamples are easy compared to proofs which require new mathematics. GenAI is great at combining existing things in new ways (interpolation). It's terrible at creating new things from scratch (extrapolation).

>GenAI is great at combining existing things in new ways (interpolation). It's terrible at creating new things from scratch (extrapolation). I think you believe a fallacy about how human cognition works if you think we actually do something different than interpolation

I think this is somehow related to GenAI’s issue of “confident incorrectness”. I’ve been trying to prompt GenAI with some highly challenging prompts recently, especially terse ones:

> Which Anjunabeats and Anjunadeep compilations have the most breakbeat tracks?

GenAI was able to give me breakbeat tracks that were on the Anjuna labels, but it completely flubbed on whether and which those tracks were on compilations. It was very confidently, mostly incorrect.

I think this is somehow isomorphic to the “interpolation vs extrapolation” issue. GenAI is forced to generate an answer, and there’s no mechanism by which we can interrogate the model for its confidence (at least, that’s my understanding).

And yet, I asked “How confident are you in your answer along different dimensions, ie whether those tracks are breakbeat, whether they are Anjuna tracks, or whether they are on those compilations?”

And its answer was surprisingly satisfying, it only gave 30% confidence that the tracks were on the compilations, which is where it flubbed.

Anyway, personal observations, GenAI is meant to be interacted with, not just a single prompt black box.

Re: Human mathematicians are being outcounterexampled

#217

Post by mb7733 » Tue, Jul 21, 2026, 3:19 PM UTC

antonvs wrote: post #202

mb7733 wrote: post #190

Earlier quoted context omitted.

Constructivists would surely disagree!

In a constructive system, it’s often possible to refute a universal proposition without exhibiting a counterexample, by proving that the proposition implies falsehood. The constructivist will still object that you can’t, from that, conclude that “…therefore a counterexample must exist,” without actually providing a counterexample. But the general principle I was describing still applies - a proof often gives you insi…

To roughly repeat myself from a sibling comment: I may have been unclear. I didn't claim that the only way to disprove something in a constructive system is to produce a counterexample.

The part that I was referring to was the last statement from the OP: that "a proof of existence of a counterexample necessarily provides more insight than a counterexample". I can't imagine a constructivist would agree with that in general.

Re: Human mathematicians are being outcounterexampled

#218

Post by m3kw9 » Tue, Jul 21, 2026, 3:20 PM UTC

Math seem like the most base thing AI will dominate first.

Re: Human mathematicians are being outcounterexampled

#219

Post by mb7733 » Tue, Jul 21, 2026, 3:26 PM UTC

Jweb_Guru wrote: post #201

mb7733 wrote: post #190

Earlier quoted context omitted.

Constructivists would surely disagree!

As a constructivist: we don't disagree :) We just distinguish between "don't disagree" and "agree." Constructive mathematics says it's fine if you want to claim that there's not no counterexample -- you just can't use that in a situation that demands an actual counterexample (like an algorithm that produces a result). This tends to guide people towards looking for results that don't require this kind of indirection,…

Maybe I was unclear. The part that I meant a constructivist would disagree was the subjective part: "This kind of proof (existence of a counterexample) provides more insight into the problem than simply finding a counterexample."

I find it hard to believe that a constructivist would agree that across the board, proof of existence of X is more interesting than a construction of X. Isn't that the point!?

Re: Human mathematicians are being outcounterexampled

#220

Post by noslenwerdna » Tue, Jul 21, 2026, 3:31 PM UTC

Diogenesian wrote: post #203

noslenwerdna wrote: post #198

Earlier quoted context omitted.

This is a very close minded definition of evil. What is the threshold of environmental impact before something is evil and its use indefensible? What level of copyright violation will send us to hell?

I didn't give a definition of evil, so "close-minded definition" is just a dishonest way of expressing that you subjectively disagree with me. Likewise with trying to make me judge an objective threshold for pollution. It really should be that any polluter needs to morally justify their actions. I find "mostly illusory productivity improvements in white-collar employment" to be an especially indefensible reason for f…

Obviously I mean the definition of evil implied by your statement that they are indefensibly evil...

Again, what level of copyright violation is evil? Downloading music without paying for it? Apparently using images/text that artists have made public is evil, so I'm curious what the bar is here for evil.

Using electricity to improve white collar efficiency is also evil. Good to know