HN

Need help?
<- Back
Human mathematicians are being outcounterexampled

Human mathematicians are being outcounterexampled

artninja1988

Comments (145)

  • Dove
    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 was the sort of thing that he really wanted to be true; he liked things smooth and beautiful. I, on the other hand, hoped it was false as I like the weird and exceptional in mathematics. It was also the case that I had absolutely no command of the sort of machinery that one would use to prove such a thing, but I could certainly look for a counterexample.I learned on Monday that he had spent the entire weekend trying and failing to prove it. I, on the other hand, had put all my energy into finding a counterexample and had one within an hour.My single (quite small) contribution to mathematical research was a counterexample because it was all I could do. The story does illustrate that it can be helpful to have people with different tools, hopes, and motivations working on a problem, though. I was not, and will never be, even a shadow of that great mathematiciam I studied under, but on that occasion, I had reason to look in a different direction than he did.
  • hintymad
    > The Jacobian ConjectureInterestingly, Yitang Zhang of the twin-prime-conjecture fame spent 7 years working on the Jacobian conjecture under the advisor Tzuong-Tsieng Moh at Purdue. A key step in his thesis used a corollary of Moh's. It turned out that the corollary was incorrect. As a result, Moh refused to write any recommendation letter for Zhang, and Zhang couldn't find any teaching or research job and ended up spending years working at a Subway[1].Imagine Zhag had ChatGPT in 1986 when he started working on the Jacobian Conjecture.[1] Of course now this has become an inspiring story. That said, the story definitely invokes complex emotions. The best way to describe it is probably this Chinese poem, which I have no idea how to translate: 庾信平生最萧瑟，暮年诗赋动江关
  • satvikpendem
    That's a good thing. It saves people wasting time trying to prove something they now know to be false, so that they can move on to other things to prove, it's a more fruitful use of humanity's time overall at least in the field of mathematics.
  • FabHK
    BTW, counterexamples in mathematics are really important and often help to refine definitions and sharpen proofs.1) I recommend the wonderful 1976 book Proofs and Refutations by Imre Lakatos.2) There is a considerable list of books dedicated to counterexamples, e.g. in topology, probability, analysis, etc.[1] https://en.wikipedia.org/wiki/Proofs_and_Refutations[2] https://www.amazon.com/s?k=counterexamples
  • dzdt
    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
  • vlovich123
    > 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 was not paying $200 per month to access these tools was crazy. In fact during the workshop I learnt from Harvard PhD student Bryan Wang that Harvard were already giving free Fable access to all PhD students, post-docs and faculty at Harvard.Yeah, given how much it accelerates grad students to produce meaningful output more quickly, why wouldn’t you make an investment of $2400/student/year. Seems like pennies overall.
  • angry_octet
    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.
  • elias_t
    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
  • bee_rider
    How do mathematicians view counter examples? Is it like an unexpected result in the physical sciences: annoying in the moment but potentially stupendously important as it reveals some inaccuracy in the current models? Or is it more like a bug report in coding… probably just, another little annoying detail?
  • VladVladikoff
    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 just proving what was already known?
  • blueTiger33
    as someone who loves math, I want to collaborate with mathematicians to solve some hard problems
  • ykonstant
    Rest in Peace those of us unable to afford those models.
  • amelius
    Next step: "the AI can't find a counterexample, so the conjecture must be true!"
  • CurtMonash
    A large fraction of the problems assigned in the Ross Program were of the form "Prove or disprove, and salvage if possible." The rest were usually a calculation, meant to motivate a general proposition you would encounter soon after.
  • mynegation
  • wizzwizz4
    Human mathematicians have been being out-counterexampled for at least two decades. The main difference, as I understand, is that (A) we now have a lot more compute to throw at such things, and (B) it is currently trendy to do so. But the sizes of counterexample we're seeing are around about what I'd expect pre-generative-AI counterexample search systems to be able to find.It's not easy to find a counterexample to the Jacobian conjecture, by any means – by which I mean to say that naïve brute-force search will take too long – but the scope of existing searches listed on Wikipedia[0] suggest that many tricks are already known, and that people just hadn't looked, systematically, for a counterexample in three variables before. Wikipedia writes:> Tzuong-Tsieng Moh checked the conjecture for polynomials of degree at most 100 in two variables.[17][18]where reference 17 is from 1983, and reference 18 is a preprint with no given date. Knowing very little about this problem, my impulse is to side with the unnamed faculty member cited in the article:> [who] said to me that the fact that the counterexample was so easy to find just indicated that humans had not spent enough time thinking about the problem,For context, the auto-generated counterexample is in three variables, has degree 7, and was discovered in 2026.
  • anon
    undefined
  • luciana1u
    the AI doesn't even gloat. a rival mathematician would at least title their paper 'a remark on the falsity of...'
  • korbonits
    Which conjectures will be proven false via counterexample next? Dixmier? Poisson?
  • QuesnayJr
    If the poster's (is it Kevin Buzzard?) suggestion works out and AI finds a counterexample to the Hodge conjecture, that would be a really big deal. It's one of the Millenium problems, for example.One thing that he mentions that already quite surprising is that AI was able to autoformalize the Golod-Shaferevich theorem and proof.
  • paulpauper
    mathematicians have been using computers for well over half a century, but this was after "bounding" the problem first and then running through the cases with a computer. Now AI is doing the first part. However, mathematicians are still needed at crafting prompts, and knowing where to look, still. The prompt for the Jacobian conjecture was obviously not random. the search space is too big to just try all the combinations of 3 variable polynomials.
  • nephihaha
    "Outcounterexampled": there's a neologism worthy of German.
  • veunes
    [flagged]
  • riazrizvi
    The framing in these posts is nonsense. ChatGPT isn't doing shit. Human mathematicians using ChatGPT are breaking boundaries.