I've been disappointed by this community before but this is the first place that there is such unanimous rejection of the very ideals the uses here will claim to represent. The reaction is just... small, tiny, petty.
24,868 karma · joined September 26, 2015
What is reasoning?
In computer science and AI when we say "reasoning" we mean that we have a theory and we can derive the consequences of the theory by application of some inference procedure.
A theory is a set of facts and rules about some environment of interest: the real world, mathematics, language, etc. Facts are things we know (or assume) to be true: they can be direct observations, or implied, guesses. Rules are conditionally true and so most easily understood as implications: if we know some facts are true we can conclude that some other facts must also be true. An inference procedure is some system of rules, separate from the theory, that tells us how we can combine the rules and facts of the theory to squeeze out new facts, or new rules.
There are three types of reasoning, what we may call modes of inference: deduction, induction and abduction. Informally, deduction means that we start with a set of rules and derive new unobserved facts, implied by the rules; induction means that we start with a set of rules and some observations and derive new rules that imply the observations; and abduction means that we start with some rules and some observations and derive new unobserved facts that imply the observations.
It's easier to understand all this with examples.
One example of deductive reasoning is planning, or automated planning and scheduling, a field of classical AI research. Planning is the "model-based approach to autonomous behaviour", according to the textbook on planning by Geffner and Bonnet. An autonomous agent starts with a "model" that describes the environment in which the agent is to operate as a set of entities with discrete states, and a set of actions that the agent can take to change those states. The agent is given a goal, an instance of its model, and it must find a sequence of actions, that we call a "plan", to take the entities in the model from their current state to the state in the goal. This is usually achieved by casting the planning problem as pathfinding over a graph with a search algorithm like A*. Here, the agent's model is a theory, the search algorithm is the inference procedure, and the plan is a consequence of the theory. Deductive reasoning can be sound, as long as the facts and rules in the theory are correct: from correct premises we can deduce correct conclusions. We know of sound deductive inference rules, e.g. A*, and Resolution, used in automated theorem proving and SAT-Solving, are sound.
The classic example of inductive reasoning is inferring the colour of swans. Most swans are white (apparently) so if we have only seen white swans we have no reason to believe there are any other colours: we are forced to infer that all swans are white. We may only be disabused of our fallacy if we happen to observe a swan that is not white, e.g. a black swan. But who is to say when such a magnificent creature will grace us with its presence, outside of Tchaikovsky's ballets? Induction is thus revealed to be unsound: even given true premises we can still arrive at the wrong conclusions. Another example is the scientific method: imagine an idealised scientist, perfectly spherical, in a frictionless vacuum. She starts with a scientific theory, then goes out into the world and makes new observations about a phenomenon not described by her theory. She constructs a hypothesis to extend her theory so as to explain the new observations. The hypothesis is a set of rules, where the premises are the consequences of the rules in her initial theory. Then, being an idealised scientist, she goes looking for new observations to refute her hypothesis. Science only gives us the tools to know when we're wrong.
Abductive reasoning is the mode of inference exemplified by Sherlock Holmes. We can imagine Sherlock and Watson standing outside a tavern in London, watching as a gentleman of interest steps out of the tavern with egg on his lapel. "Ah, my dear Watson, what can we conclude from this observation?". "Why my dear Holmes, we can conclude that the man had eggs for breakfast". Holmes and Watson can arrive at this conclusion, about a fact that they have not directly observed, because they have a theory with a rule that says "if one eats eggs, one may get some on one's lapels". Working backwards from this rule, and their observation of egg on the man's lapels, they can guess that he had eggs even if they didn't directly observe him doing so. Abduction is also unsound: the man may have swapped coats with an accomplice, who was the one who had eggs for breakfast instead.
And now you know what "reasoning" means. So the next time someone asks: "what is reasoning?", you can let them know and turn the discussion to more interesting, more productive directions.
I've been disappointed by this community before but this is the first place that there is such unanimous rejection of the very ideals the uses here will claim to represent. The reaction is just... small, tiny, petty.
To clarify, they do attribute the original ideas to Cordoba and Martinez-Zoroa, but they don't seem to acknowledge that their result which they say was achieved "with a great deal of help from LLMs" is also derivative of others' work.
Independence is about avoiding making errors because of the influence of error-prone models. I guess I didn't explain it well.
One reason not to try is to create an air gap between the OP's ideas and the data that future models can train on. We saw that the mathematicians who trusted OpenAI and Anthropic with their preliminary work found the rug pulled out of their feet by those same companies.
Another reason is to avoid inadvertently plagiarising the work of other mathematicians. Any mathematical insight that comes out of an LLM is the result of training on the entire bibliography of mathematical research, but those insights are spat out of the models without attribution. If you use AI in your matematical research you are only using the work of others without even knowing who they are and what they contributed.
And yet another reason is to avoid polluting your mind with the ideas that come out of the AI. Maybe you get a hint that pushes you to one direction, when you would go into an entirely other direction without that hint. And then maybe that becomes a habit and you can't find new directions without asking the all-knowing oracle.
tl;dr: opsec, integrity and independence are the reasons to not use LLMs in your research. I don't.
I need to be very precise here, but it is not right to say that we know what the best move is in any chess board position. What we know is what move a chess engine would make that would win the game against a human, or sometimes another chess engine. We know a winning move; not the best move.
Winning in chess is not the same as knowing what the best move is. Having chess engines that can beat any human in chess is not the same as knowing how every possible game will develop. The latter is known as "solving chess" and we don't yet have that. We have fully solved games like tic-tac-toe, backgammon and checkers, so that there exist databases of every possible path through those games but this is not done for chess, and there is no hint that it is even possible to do given that chess is such a combinatorially more complex game than those.
More to the point, the upshot of the fact that we now have super-human chess engines that can beat any human in chess (and Go and shoggi) is that there is no longer the will to research the bigger question about solving chess. The solution of the minor problem, how to beat humans in chess, has sidelined and displaced research in the major problem, how to solve chess, and we will now never find the solution to the latter.
And if that reminds you of something, well, yes, exactly.
Genuine question: who were those people saying that? I don't know that criticism.
The criticism I know is from AI researchers and it is that beating humans at chess using a computer running an algorithm unlike anything that humans do when they play chess, tells us nothing about the way that humans play chess, which is what we are trying to understand when we try to get computers to play chess.
This criticism is exemplified by John McCarthy's article (the real godfather of AI; because he named it) "Ai as Sport" whence I quote:
Ideas about chess algorithms as well as advances in computer hardware were involved. However, it is a measure of our limited understanding of the principles of artificial intelligence (AI) that this level of play requires many millions of times as much computing as a human chess player does. Moreover, the fixation of most computer chess work on success in tournament play has come at scientific cost.
In 1965 the Russian mathematician Alexander Kronrod said, "Chess is the Drosophila of artificial intelligence." However, computer chess has developed much as genetics might have if the geneticists had concentrated their efforts starting in 1910 on breeding racing Drosophila. We would have some science, but mainly we would have very fast fruit flies.
https://www-formal.stanford.edu/jmc/newborn/newborn.html
A more recent criticism that can be made is that getting computers to beat humans at chess (and later Go, and Shoggi and Atari and Stratego) has turned out to only be possible with techniques that are too narrow to have real-world application. Btw, this includes Reinforcement Learning which is still much more capable in virtual environments than in any real-world environment.
I'll wait until there's more concrete information.
Do the job yourself. And if you can't, that's maybe a hint that you should listen to the people who can.
Presumably you're a human. Are you going to do that?
Where did I say that?
The conversation you seem to want to have doesn't seem to have any obvious use and you seem to want to debate a point I never made. I don't seem to be needed here so I will now bow out of the conversation.
It's the tools that produce the works, not the humans.
>> This is a horrible perversion of the quote.
What? The full quote is "Those are brave men knocking at our doors. Let's go kill them!". What's the perversion?
I don't know what you should do because I'm not a mathematician. But superintelligence schmuperintelligence. We didn't stop running because we have cars or playing chess or Go because there's chess and Go engines. Even more so than chess there's no point in maths unless it's people doing it, for other people. AI maths makes no sense, like AI art makes no sense, because those are things that people enjoy and can do pretty damn well ourselves so there's no point to automate them away. We gotta stop that bullshit, and we can stop it. And if we don't, if we just sit around and wait for OpenAI and Anthropic to destroy society then that's not their fault but ours.
Sorry, I'm not great at pep talks. Those are brave men. Let's go kill them!
*Jingle-jangle fallacies are erroneous assumptions that either two different things are the same because they bear the same name (jingle fallacy); or two identical or almost identical things are different because they are labeled differently (jangle fallacy).[1][2][3] The term was coined by Truman Lee Kelley in his 1927 book Interpretation of educational measurements.[4] In research, a jangle fallacy is the inference that two measures (e.g., tests, scales) with different names measure different constructs. By comparison, a jingle fallacy is the assumption that two measures which are called by the same name capture the same construct.[5][6][7]
And people thought Experts Systems were bad.
It's perhaps great in the short term although it's not very clear who it's great for. I'm not sure mathematicians find it all so great, I mean.
In the long term, if this contrives to destroy the tradition of human mathematics the whole endeavour is self-defeating. In time, there will be nobody left with the knowledge and skills to produce mathematics to train AI to do mathematics.
And then we'll be left with no mathematics at all: we'll have no human mathematicians and no AI that can do mathematics, either.
Maybe I'm failing to read that graph properly but the y axis says "pass rate" and it only goes up to 0.5. That would mean every single problem is at most half-solved.
I don't know what that means though. What is "0.5 pass rate" in the context of "open math problems" (as in the graph title)?
There was much excitement, then, as now, for this kind of approach and there were several systems that followed along the same lines, e.g. Automated Mathematician by Doug Lenat.
Eventually it became clear that this approach is limited by what it can generate: you may have a sound and complete verifier, but if the generator, i.e. the first step in the generate-and-test pipeline, is incomplete, then the entire thing will run out of steam sooner or later.
The difference with LLMs is that they are... well, large. They are the most powerful generators ever created. That means their limits are not in sight and it will probably take us a very long time to find them.
Which is all to say that, yes of course, automatic verification is indispensable. But without an LLM generating an unprecedentedly large number of plausible theorems, there would be no AI mathematics, or in any case AI mathematics wouldn't have gone as far as it has.
I can't progress beyond this point in the article. How is Waymo's study "independent"? I don't understand.
Also brain raping* is not illegal in most jurisdictions.
But they're both deeply disturbing.
_________
About the plagiarism issue, I model it as OpenAI being an advisor and their AI a PhD student. If the advisor puts their name on a paper behind that of their PhD and it turns out the PhD copied the text of the paper from somewhere else the advisor is also responsible of plagiarism, not just the student. The least the advisor can do is withdraw their authorship from the paper.
But, yeah, point well made: it could be much worse than that. Like an advisor instructing a student to copy someone else's paper.
How "fast" does it have to be? Buckmaster and Alpoge have been working on this for just a day short of a year. See Alpoge's tweet announcing his collaboration with Bukmaster dated 9/19/25:
https://x.com/__alpoge__/status/2097206973418611054
It takes a few months to train a model these days but not a whole year. OpenAI had all the time to train on Buckmaster and Alpoge's results of just a few months earlier at which point they must have been well on the path to their result.
It's a bit like sending unencrypted messages through a messaging app and the developer having a TOS that says they don't look at your messages. They might not, but they are fully capable of doing so. If they have a reason to do it, they will. Nobody's stopping them.
This sounds like a very big coincidence and it looks really bad for OpenAI but there is an alternative explanation that I can only state as a conjecture.
Suppose that the ability of LLMs to generate mathematical proofs is like a quiver full of arrows: each arrow, one proof. The same quiver is shared between all instances of one model and substantially similar models share substantial subsets of the arrows in the same quiver.
That would allow two independent teams to converge on the same LLM-aided solutions to the same problems. Even more likely so if the quivers were small and finite and their arrows were specific to a distinct class of problems (without being able to suggest a particular class from what we've seen so far).
This would explain the kind of LLM-mediated results we've seen so far that tend to be ... sparse. By which I mean that every time there's a new model release we get some new results and then they seem to dry out, until the next release.
It would also explain how OpenAI was about to prove the same result as Buckmaster and Alpoge, while absolving OpenAI of any misconduct. And this is one reason to prefer this explanation: one should not favour accusations of misconduct as long as there are conceivable alternatives.
But, that's just a conjecture that I can't prove.