Login
You're viewing the f.duriansoftware.com public feed.

Replies

  • Oct 8, 2026, 1:01 PM

    I feel this is getting a disproportionate amount of attention on here, relative to the 369 papers that haven't been withdrawn

    💬 5🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • Oct 8, 2026, 1:20 PM

    @robinhouston I've noticed (with equal parts amusement and despair) that the bar for AI 'doing' maths is now sufficiently high ("What new ideas has it developed to prove that theorem?") that it excludes the vast majority of all published mathematics papers, and probably of published mathematicians.

    💬 0🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • Oct 8, 2026, 1:25 PM

    @Diffgeometer1 I don't like that either, but there are still some pretty interesting claims in there, and I bet most (not all) of the remaining proofs will hold up.

    💬 2🔄 0⭐ 0
  • Oct 8, 2026, 3:38 PM

    @robinhouston @Diffgeometer1 What I have not seen raised in this current crisis, if people want to call it that, is the issue of whether or not mechanised so-called proofs should be used in the first place.

    The reason that, in general and as far as I know, the mathematical community has largely stayed away from tools like Lean is not because they are difficult to use. It is because a Lean program, or any other output produced by these tools, cannot communicate mathematical intent. It is like giving the source code of a video game to a player and asking them to wring what pleasure they can out of reading it. It doesn't matter how well documented or orderly the code is, it is just not the same thing. I am probably preaching to the converted in making this rather clumsy analogy, but still...

    Why bother training models to output Lean proofs. It creates a massive representation gap and increasingly alienates and infuriates mathematicians. Why not just output readable proofs written for TeX? Isn't that a big enough representation gap?

    Why this obsession with Lean programs? This is the crisis, that mathematicians haven't turned around to the AI community and told them to come back with readable proofs.

    So called Lean certificates buy you nothing. They are barely more than a hoax. Oh, you must accept this proof because of this shiny certificate. It is borderline farcical. The last time I looked Lean hash over two thousand issues on GitHub, not all of them cosmetic.

    The next thing people will be training models to convert Lean proofs back into TeX. In fact, I bet it is already happening. As I said, borderline farcical.

    💬 0🔄 0⭐ 0
  • Oct 8, 2026, 9:57 PM

    @robinhouston is it asking OpenAI too much to post the papers on arxiv where there’s a permanent record of their work and people can study it and vet it?

    Or how about they submit their papers to journals for peer review?

    It’s a super rich company. It’s totally within their ability. Or is their primary motive to keep generating headlines so they can keep milking their investors?

    💬 0🔄 0⭐ 0
  • Oct 8, 2026, 1:26 PM

    @robinhouston If a human mathematician who’d submitted over 300 papers in a single year was shown to be rushed and incorrect in three of them, what do you think the community would do with the rest?

    Would that human be lauded and praised for the remaining 99% of the work, sight unseen; or would every one of the papers instead be scrutinized twice as thoroughly?

    💬 0🔄 0⭐ 0
  • Oct 8, 2026, 2:27 PM

    @robinhouston Wait, didn't they sent out 700+ papers. Why are you talking about 369 that weren't retracted?
    (There is a good chance I just missed or misinterpreted something.)

    💬 1🔄 0⭐ 0
  • 💬 2🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • Oct 8, 2026, 3:42 PM

    @robinhouston - Many people treat what's going on as a battle between AI and human mathematicians, and are happy to see AI losing even a few battles here and there. It reminds me of how I felt during the early days of the big Russian invasion of Ukraine. Soldiers were heroically holding out in the steel mill in Mariupol, etc.

    My own feelings are a bit different. I dislike OpenAI mightily, but I think humans can enjoy doing math even as AI becomes arbitrarily good, and I plan to be involved as long as I've got enough pep to do math.

    💬 1🔄 0⭐ 2
  • 💬 1🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • OddOpinions5failedLyndonLaRouchite@mas.to
    Oct 8, 2026, 3:43 PM

    @robinhouston
    @oantolin

    I'm just some internet rando, but I have the impression that it has never happened before that errors, of one sort or another, happened in the a early stage of some tech, or that there was no hype associated with an early state tech

    💬 0🔄 0⭐ 0