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

151–160 of 265 posts

Re: Human mathematicians are being outcounterexampled

#151

Post by avianlyric »

OscarCunningham wrote: post #126
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

They're trained on human data. I would expect them to emulate human biases as closely as possible.

This is where harness, and the fact that a machine can be endlessly prompted to try again comes in.

Even if an LLM starts by pursuing things that follow human bias, continuous failures and re-prompting to try something different will eventually force it to consider things outside of what ever biases it has.

You can do the same thing to a human. But most people would consider it unethical to lock someone in a box and force them to keep trying to solve the same problem over and over again until they figure it out.

Re: Human mathematicians are being outcounterexampled

#152

Post by saagarjha »

murphyslaw wrote: post #112
AndrewKemendo wrote: post #75

Earlier quoted context omitted.

I couldn’t get the video to work. Here’s the relevant clip I found on youtube. https://youtu.be/3uRCcEoGWxs

BBC iPlayer is not available outside the UK.

It worked fine for me in the US

Re: Human mathematicians are being outcounterexampled

#154

Post by antonvs »

mb7733 wrote: post #43
SpicyLemonZest wrote: post #32

Earlier quoted context omitted.

It’s very straightforward, but it often doesn’t (and here didn’t) fully satisfy the curiosity that was embedded in the original problem. Why did the Jacobian conjecture seem to be true? Is there some underlying symmetry that’s very slightly broken? Or perhaps there’s all kinds of counterexamples, and the intuitive pattern is only real for certain kinds of functions which happen to predominate in our intuition. Then h…

Those are all good questions, but I don't really understand what alternative you or the OP are looking for actually resolving an untrue conjecture, besides a counter example.

There are many cases where it's possible to prove that counterexamples must exist, without identifying a specific example. This kind of proof provides more insight into the problem than simply finding a counterexample.

Re: Human mathematicians are being outcounterexampled

#155

Post by refactor_master »

veunes wrote: post #118
Dove wrote: post #15

When I was in grad school, I had the opportunity to take a course from my adviser in which he discussed his current research and some open questions. It was a relatively accessible subject area and the questions were sometimes easy enough that we could meaningfully contribute. On one particular Friday afternoon, he stated a conjecture that he hoped was true, and invited us to try to help him prove or disprove it. It…

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

This reminds me of the Go Grandmaster speaking out after losing to AlphaGo, that the model has no sense of "aesthetic play", as long as it would lead to a win within the rules.

Re: Human mathematicians are being outcounterexampled

#156

Post by Xmd5a »

bananaflag wrote: post #125
tchalla wrote: post #24

Earlier quoted context omitted.

I was once in a presentation for a math PhD thesis. During the thesis, the evaluator of the thesis noticed a flaw in their proof. The student understood and then asked “What now?” The evaluator prof simply shrugged.

I personally know a story in this vein with a (sort of) happy ending. A PhD student discovered that a result of his professor would imply the solution to a big conjecture in another field. The people in that field then analyzed the prof's result and found that the proof was flawed. The student was still allowed to graduate based on this since the finding of the connection between fields was brilliant. Then he quit ac…

> The two are still on good terms, writing papers together.

Why are you framing this like this? Do mathematician take these kind of things personally?

Re: Human mathematicians are being outcounterexampled

#157

Post by IngoBlechschmid »

angry_octet wrote: post #57

I wish I had LLM-built Lean formalisations in university, so much of the math in the slides had errors, and some professors are very bad and ungracious admitting it, while simultaneously rejecting requests for clarifications by saying "the proof is in the slides". Of course Lean proofs are rarely a good way to understand proofs, but hopefully they can be used to generate more human understandable arguments.

> Of course Lean proofs are rarely a good way to understand proofs, but hopefully they can be used to generate more human understandable arguments.

I would object to the first part: Of course there is a nontrivial learning curve, but then I'd argue that non-slop Lean/Agda/Rocq/... formalizations are amazing for understanding proofs. A good formalization presents the outline and the key arguments in nicely structured form, and then, unlike pen-and-paper proofs, also allow you to get the details on every single step, exactly to your desired level of depth.

The proofs in Martín Escardó's TypeTopology Agda repository come immediately to my mind as an example. [An interactive Agda tutorial is here: lets-play-agda.quasicoherent.io]

In contrast, LLM-generated formalizations can currently be extremely messy. They certify truth and can also contain interesting arguments, but substantial work is required to bring them into a shape that contributes to the actual goal of improving our understanding of the mathematical landscape.

Re: Human mathematicians are being outcounterexampled

#158

Post by bananaflag »

Xmd5a wrote: post #156
bananaflag wrote: post #125

Earlier quoted context omitted.

I personally know a story in this vein with a (sort of) happy ending. A PhD student discovered that a result of his professor would imply the solution to a big conjecture in another field. The people in that field then analyzed the prof's result and found that the proof was flawed. The student was still allowed to graduate based on this since the finding of the connection between fields was brilliant. Then he quit ac…

> The two are still on good terms, writing papers together. Why are you framing this like this? Do mathematician take these kind of things personally?

Because I think the median reader would expect this sort of thing to come up at some point in the story.

Re: Human mathematicians are being outcounterexampled

#159

Post by Diogenesian »

dzdt wrote: post #40

I suppose it will fall to AI as well to compose the mathematical equivalent of The Ballad of John Henry. Who will be the human champion, the last great hero who can deliver proofs "from the book" that a machine cannot outperform? [1] https://en.wikipedia.org/wiki/John_Henry_(folklore) [2] https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

This is an unhealthy view of mathematics. It's mathematics as envisioned by football fans.

The most valuable things in mathematics are not beautiful proofs. We need more useful definitions. Actually coming up with useful definitions (and building good conjectures out of them - not even theorems, conjectures) is something LLMs have not yet tried to conquer.

Re: Human mathematicians are being outcounterexampled

#160

Post by Diogenesian »

vlovich123 wrote: post #71

> A few days earlier I had got an email from a professor in the maths department here at Imperial, expressing surprise that some of our graduate students were paying $200 per month to access models such as Sol and Fable. He said that he thought that these people were crazy. I did not immediately respond. But after meeting with Andrew I emailed the professor back and told him that in my opinion, any PhD student who wa…

Many graduate students view themselves as ethical beings, not machines that "produce meaningful output," and everybody here knows (useful) LLMs are indefensibly evil because of stolen training data and enormous environmental impact.
Post reply on HN