Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Human mathematicians are being outcounterexampled

xenaproject.wordpress.com

Post reply on HN
Print view View original

231–240 of 265 posts

Re: Human mathematicians are being outcounterexampled

#231

Post by Jweb_Guru »

mb7733 wrote: post #219
Jweb_Guru wrote: post #201

Earlier quoted context omitted.

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!?

A direct counterexample is more "informative" in a very literal sense (its truth value doesn't collapse). But the extra proof relevant content we can use here is not that large -- all it means in this case is that we can directly compute the object and its Jacobian, a well as two points evaluating to the same result. That's nice, but it's not that interesting by itself unless I can use the exact constructed form to prove other interesting stuff (and we can! Most of the followup results that immediately followed from the disrpoof come from being able to directly transform this object into counterexamples to other conjectures; if we didn't have constructive proofs of thoe counterexamples, we wouldn't have such procedures). But being more interesting than a completely uninformative counterexample still doesn't mean it's inherently interesting or enlightening. If anything I'd indeed argue constructive arguments are generally less mysterious and magical than nonconstructive proofs -- in some sense, the constructive proof pulls back the curtain and shows you where the trick is.

Re: Human mathematicians are being outcounterexampled

#232

Post by antonvs »

Jweb_Guru wrote: post #209
antonvs wrote: post #202

Earlier quoted context omitted.

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…

I think the constructive position is basically that people's entire issue with lack of excluded middle being absent is just that people like being able to say "P" instead of "~~P" because it sounds better, considering you can prove ~~P for all the classical propositions that use excluded middle.

> people like being able to say "P" instead of "~~P" because it sounds better

It depends on how old an intuitionist/constructionist you are. Back in the day, they were interested in logic as a description of correct reasoning. Brouwer saw LEM as a mistake in the foundations.

These days, the influence of formalization, including proof theory and model theory, has removed a lot of the teeth from that debate and made it possible to summarize as you have.

I studied this in the early 1980s, and my professor was definitely in the "this is a black and white issue" camp, although he came down on the classical side.

(Side note, I was once a back seat passenger in a car with my prof and Quine in the front seat, who was visiting at the time. Quine was famously committed to the idea that first order logic is the only kind worthy of the name.)

Re: Human mathematicians are being outcounterexampled

#233

Post by ted_dunning »

t-3 wrote: post #149
somenameforme wrote: post #143

Earlier quoted context omitted.

A fee charging privately operated institution that does not receive public funding. [1] Brits have a way with words. [1] - https://en.wikipedia.org/wiki/Public_school_(United_Kingdom)

The US still somewhat has a similar distinction with public and private colleges. Private vs public funding rather than private vs public admission .

A similar distinction with opposite polarity, however.

A public school in Britain does not receive public funding.

A public school in the US is entirely publicly funded.

Re: Human mathematicians are being outcounterexampled

#234

Post by gabriel666smith »

VladVladikoff wrote: post #17

A lot of this math is beyond my comprehension, but it often seems to talk of proofs of theorems. What I want to know is if we continue on this accelerated AI mathematics trajectory, will we eventually be discovering new forms of math that will in turn have some applications down the line in engineering or biomedicine etc? I guess what I’m asking is are we on the cusp of a huge breakthrough for humanity, or largely ju…

You can personally work out how apply this one in engineering today!

If you have a spare hour or two, I'd encourage you to have a go at learning (however you learn best - I like just asking smarter people or robots stupid questions) what the maths means and why it's important.

And then once you feel like you have a vague grip on the principles, think about a problem in a domain you know a lot about. Try to see if the maths - and how it's changed our perception - could be used as a tool to solve that problem, or if the solution is analogous to a solution you could try in your own domain of expertise.

LLMs are good at speeding up, I think, the journey an idea has to take between "theoretical academic stuff for academics" and "a usable idea for regular people", because they increasingly allow you to ask an infinite number of stupid questions and give you (hopefully) reasonably good responses.

I've had loads of fun doing this today - specifically seeing if the idea this counter (from what I understand: a many-to-one conversion that kind of does and kind of does not preserve meaning) can tell me anything about the relationship between language and meaning.

I'm sure everything I've done today while mucking around has been the equivalent of a monkey with a typewriter (and Codex), but I think the huge breakthrough(s) you ask whether we're on the cusp of are relatively dependent on how many monkeys are throwing typewriters at problems they know a little bit about, after learning a bit about new ideas like this one. Historically, that's a really good way for broad cultural innovation to happen - distributed information applied across multiple domains by experts in them.

Re: Human mathematicians are being outcounterexampled

#235

Post by datsci_est_2015 »

gwerbin wrote: post #227
datsci_est_2015 wrote: post #224

Earlier quoted context omitted.

GPT 5.5 > IMO harnesses need some kind of built in "are you sure about that?" loop checkpoint that pauses the main interaction and asks the LLM to evaluate the strength of evidence for a claim it's about to make. As a practitioner of ML for the past decade, this is the part of LLMs that has always been least satisfying for me. The shared intuition amongst myself and my colleagues has always been that the strongest mo…

I find this perspective surprising coming from someone who's done ML for a decade. How much of a good machine learning system in production is really "the model"? How many lines of code are dedicated to constructing features and preprocessing them? How many lines are needed to process the decision emitted by the model in context of whatever else is going on? How often does the customer interact directly with the infe…

It’s a fair perspective that you’re bringing, but what comes to mind for me in response is that I have a mental model of two types of machine learning inferences that provide value:

Type B: “directionally correct” ML inferences that provide value by virtue of outputting an inference regardless of its accuracy. The value comes from providing automated decision that allows someone or something to move forward in a process, similar to management consultants. This is used heavily in ad tech and (social) media algorithms. I would even put gambling and investing inferences in this bucket as the accuracy of algorithms isn’t really required to be that high to provide alpha.

Type A: ML inferences that are creating or replacing systems where high accuracy is table stakes. This is applications in industrial engineering, chemical engineering, biotechnology, etc. If you can’t beat any existing automated or non-automated systems in terms of accuracy, your product is dead in the water. You can make it a few years by faking it but eventually the pied piper makes his call, and a major contract falls through. This has always been the lifecycle of products I’ve been on. It’s an incredibly difficult problem. “Faking it” here means piling on heuristics upon heuristics to convince someone to sign a contract, even if the underlying precision-recall tradeoff curve isn’t financially viable. This is the basis for the conversations between myself and my colleagues that a model that can’t provide actionable insights without a wall of heuristics / post-processing is a red flag for a product.

Anyway, that generalizes to LLMs because LLMs can provide so much value in the Type B category, but anyone promising Type A products based on LLM technology is treading on thin ice, imo.

Edit: also, as an aside, feature extraction and post-processing of inferences is necessary for any model, but if that code becomes bloated is when I lose confidence in the model’s ability to provide inference value.

There’s a classic stack overflow from a decade ago that I remember where a ML engineer / DS was asking if a linear regression model trained on sorted data (X, Y sorted independently) had any inference value. They asked because their manager insisted that was the correct way to do it because it minimized training error. Well, duh. Two sorted lists of values are maximally correlated.

This is an extreme example of what I mean by “preprocessing data”.

An extreme example of “postprocessing results” would be to create a decision tree based on the output of a decision tree algorithm that re-sorts values into something that is palatable for the customer, based on feedback from the customer on a case-by-case basis. “Hey this was a false positive…” -> add an “if” statement to the postprocessing.

Re: Human mathematicians are being outcounterexampled

#236

Post by tantalor »

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

Then where do new ideas come from? Do the muses bestow divine creativity upon artists, poets, and musicians?

Re: Human mathematicians are being outcounterexampled

#237

Post by evenhash »

vlovich123 wrote: post #89
adw wrote: post #80

Earlier quoted context omitted.

The living-costs stipend for an EPSRC PhD student is around £20k so it's about ten percent of that... big commitment for a student to make!

Which is why the school should be covering it.

It would be better to just give the students the money and let them spend it as they need.

If I were a student living on a measly $1600/month I would be livid if the school gave me a $200 raise in AI credits, instead of money to buy groceries or pay rent.

Re: Human mathematicians are being outcounterexampled

#238

Post by rowanG077 »

tantalor wrote: post #176
veunes wrote: post #118

Earlier quoted context omitted.

This is probably part of why machines are doing so well at counterexamples. They have no aesthetic commitment to the conjecture and no embarrassment about producing something ugly

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).

I really don't think that's true. Of course after the fact a counter example looks easy. Because look at it, it's obviously that it doesn't work. But that disregards the process of finding it. That requires great creativity(or computational resources if the problem is tractable at all).

Re: Human mathematicians are being outcounterexampled

#239

Post by Jweb_Guru »

antonvs wrote: post #232
Jweb_Guru wrote: post #209

Earlier quoted context omitted.

I think the constructive position is basically that people's entire issue with lack of excluded middle being absent is just that people like being able to say "P" instead of "~~P" because it sounds better, considering you can prove ~~P for all the classical propositions that use excluded middle.

> people like being able to say "P" instead of "~~P" because it sounds better It depends on how old an intuitionist/constructionist you are. Back in the day, they were interested in logic as a description of correct reasoning. Brouwer saw LEM as a mistake in the foundations. These days, the influence of formalization, including proof theory and model theory, has removed a lot of the teeth from that debate and made it…

Ah, I didn't realize this was a generational thing. I am definitely a "new" intuitionist, so that probably greatly influences my perspective. I suppose that before results like this, the setoid model, etc. were known constructivism was indeed a much more hardline position to have to take!

Re: Human mathematicians are being outcounterexampled

#240

Post by YoshiRulz »

elias_t wrote: post #213
inigyou wrote: post #167

Earlier quoted context omitted.

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?

From the article: https://mathlib.org

Also https://1000-plus.github.io and https://us.metamath.org

Post reply on HN