[HN Gopher] First Proof
___________________________________________________________________
First Proof
Author : samasblack
Score : 73 points
Date : 2026-02-07 15:25 UTC (7 hours ago)
(HTM) web link (arxiv.org)
(TXT) w3m dump (arxiv.org)
| samasblack wrote:
| https://1stproof.org/#about
| happa wrote:
| February 13th is a pretty close deadline. They should at least
| have given a month.
| blenderob wrote:
| February 13 seems right to me. I mean it's not like LLMs need
| to manually write out a 10 page proof. But a longer deadline
| can give human mathematicians time to solve the problem and
| write out a proof. A close deadline advantages the LLM and
| disadvantages humans which should be the goal if we want to see
| if LLMs are able to solve these.
| baal80spam wrote:
| I'll patiently wait for the "goalpost moving olympics" after this
| is published.
| blenderob wrote:
| The goalposts have been on wheels basically since the field was
| born. Look up "AI effect". I've stopped caring what HN comments
| have to say about whether something is or isn't AI. If its
| useful to me, I'm gonna use it.
| blenderob wrote:
| Can someone explain how this would work?
|
| > the answers are known to the authors of the questions but will
| remain encrypted for a short time.
|
| Ok. But humans may be able to solve the problems too. What
| prevents Anthropic or OpenAI from hiring mathematicians, have
| them write the proof and pass it off as LLM written? I'm not
| saying that's what they'll do. But shouldn't the paper say
| something about how they're going to validate that this doesn't
| happen?
|
| Honest question here. Not trying to start a flame here. Honestly
| confused how this is going to test what it wants to test. Or
| maybe I'm just plain confused. Someone help me understand this?
| yorwba wrote:
| This is not a benchmark. They just want to give people the
| opportunity to try their hand at solving novel questions with
| AI and see what happens. If an AI company pulls a solution out
| of their hat that cannot be replicated with the products they
| make available to ordinary people, that's hardly worth bragging
| about and in any case it's not the point of the exercise.
| cocoto wrote:
| They could solve the problems and train the next models with
| the answers, as such the future models could "solve" theses.
| fph wrote:
| The authors mention that before publications they tested
| these questions on Gemini and GPT, so they have been
| available to the two biggest players already; they have a
| head start.
| data_maan wrote:
| Looks like very sloppy research.
| YeGoblynQueenne wrote:
| Hey, sorry, totally out of context but I've always wanted to
| ask about the username. I keep reading it as "yoruba" in my
| mind. What does it mean, if I'm not being indiscreet?
| yorwba wrote:
| You're not the first to have wondered:
| https://news.ycombinator.com/item?id=20730027
| YeGoblynQueenne wrote:
| Well, now that I read that comment I remembered having
| read it before. My mind is going.
| conformist wrote:
| It's possible but unlikely given the short timeline, diverse
| questions that require multiple matheamticians, and low stakes.
| Also they've already run preliminary tests.
| blenderob wrote:
| > It's possible but unlikely given the short timeline
|
| Yep. "possible but unlikely" was my take too. As another
| person commented, this isn't really a benchmark, and as long
| as that's clear, it seems fair. My only fear is that some
| submissions may be AI-assisted rather than fully AI-
| generated, with crucial insights coming from experienced
| mathematicians. That's still a real achievement even if it's
| human + AI collaboration. But I fear that the nuance would be
| lost on news media and they'll publish news about the dawn of
| fully autonomous math reasoning.
| iLoveOncall wrote:
| That was exactly my first thought as well. All those exercises
| are pointless and people don't seem to understand it, it's
| baffling.
|
| Even if it's not Anthropic or OpenAI paying for the solutions,
| maybe it'll be someone solving them "for fun" because the paper
| got popular and posting them online.
|
| It's a futile exercise.
| data_maan wrote:
| Nothing prevents them, and they are already doing that. I work
| in this field and one can be sure that now, because of the
| notoriety this preprint got, the questions will be solved soon.
| falloutx wrote:
| Anything special about these questions? Are they unsolved by
| humans. I am not working in mathematics research so its hard to
| tell the importance.
| jsnell wrote:
| The abstract of the article is very short, and seems pretty
| clear to both of your questions.
|
| This is what is special about them:
|
| > a set of ten math questions which have arisen naturally in
| the research process of the authors. The questions had not been
| shared publicly until now;
|
| I.e. these are problems of some practical interest, not just
| performative/competitive maths.
|
| And this is what is know about the solutions:
|
| > the answers are known to the authors of the questions but
| will remain encrypted for a short time.
|
| I.e. a solution is known, but is guaranteed to not be in the
| training set for any AI.
| blenderob wrote:
| > I.e. a solution is known, but is guaranteed to not be in
| the training set for any AI.
|
| Not a mathematician and obviously you guys understand this
| better than I do. One thing I can't understand is how they're
| going to judge if a solution was AI written or human written.
| I mean, a human could also potentially solve the problem and
| pass it off as AI? You might say why would a human want to do
| that? Normal mathematicians might not want to do that. But
| mathematicians hired by Anthropic or OpenAI might want to do
| that to pass it off as AI achievements?
| teraflop wrote:
| Well, I think the paper answers that too. These problems
| are intended as a tool for honest researchers to use for
| _exploring_ the capabilities of current AI models, in a
| reasonably fair way. They 're specifically _not_ intended
| as a rigorous benchmark to be treated adversarially.
|
| Of course a math expert could solve the problems themselves
| and lie by saying that an AI model did it. In the same way,
| somebody with enough money could secretly film a movie and
| then claim that it was made by AI. That's outside the scope
| of what this paper is trying to address.
|
| The point is not to score models based on how many of the
| problems they can solve. The point is to look at the
| models' responses and see how good they are at tackling the
| problem. And that's why the authors say that ideally,
| people solving these problems with AI would post complete
| chat transcripts (or the equivalent) so that readers can
| assess how much of the intellectual contribution actually
| came from AI.
| data_maan wrote:
| > these are problems of some practical interest, not just
| performative/competitive maths.
|
| FrontierMath did this a year ago. Where is the novelty here?
|
| > a solution is known, but is guaranteed to not be in the
| training set for any AI.
|
| Wrong, as the questions were poses to commercial AI models
| and they can solve them.
|
| This paper violates basic benchmarking principles.
| offnominal wrote:
| > Wrong, as the questions were poses to commercial AI
| models and they can solve them.
|
| Why does this matter? As far as I can tell, because the
| solution is not known this only affects the time constant
| (i.e. the problems were known for longer than a week). It
| doesn't seem that I should care about that.
| data_maan wrote:
| Because the companies have the data and can solve them --
| so providing the question to a company with the necessary
| manpower, one cannot guarantee anymore that the solution
| is not known, and not contained in the training sample.
| _alternator_ wrote:
| These are very serious research level math questions. They are
| not "Erdos style" questions; they look more like problems or
| lemmas that I encountered while doing my PhD. Things that don't
| make it into the papers but were part of an interesting diversion
| along the way.
|
| It seems likely that PhD students in the subfields of the authors
| are capable of solving these problems. What makes them
| interesting is that they seem to require fairly high research
| level context to really make progress.
|
| It's a test of whether the LLMs can really synthesize results
| from knowledge that require a human several years of postgraduate
| preparation in a specific research area.
| clickety_clack wrote:
| So these are like those problems that are "left for the
| reader"?
| Jaxan wrote:
| Not necessarily. Even the statements may not appear in the
| final paper. The questions arose during research, and
| understanding them was needed for the authors to progress,
| but maybe not needed for the goal in mind.
| data_maan wrote:
| Very serious for mathematicians - not for ML researchers.
|
| If the paper would not have had the AI spin, would those 10
| questions still have been interesting?
|
| It seems to me that we have here a paper that is solely
| interesting because of the AI spin -- while at the same time
| this AI spin is really poorly executed from the point of AI
| research, where this should be a blog post at most, not an
| arXiv preprint.
| j_maffe wrote:
| The timed-reveal aspect is also interesting.
| data_maan wrote:
| How is that interesting for a scientific point of view?
| This seems more like a social experiment dressed as
| science.
|
| Science should be about reproducibility, and almost nothing
| here is reproducible.
| richard_chase wrote:
| Interesting questions. I think I'll attempt #7.
| gre wrote:
| Tried all ten with claude, then had codex take a loook at the
| work -- codex thinks number 7 has the lowest chance of being
| correct, a 1 out of 10 rating. None of them were higher than
| 7/10 chance of being right so far as done by claude opus 4.6
| and evaluated by codex 5.3 highest.
|
| Not going to spend too many more tokens on this.
| Syzygies wrote:
| I'm a mathematician relying heavily on AI as an association
| engine of massive scope, to organize and expand my thoughts. One
| doesn't get best results by "testing" AI.
|
| A surfboard is also an amazing tool, but there's more to
| operating one than telling it which way to go.
|
| Many people want self-driving cars so they can drink in the back
| seat watching movies. They'll find their jobs replaced by AI,
| with a poor quality of life because we're a selfish species. In
| contrast Niki Lauda trusted fellow Formula 1 race car driver
| James Hunt to race centimeters apart. Some people want AI to help
| them drive that well. They'll have great jobs as AI evolves.
|
| Gary Kasparov pioneered "freestyle" chess tournaments after his
| defeat by Big Blue, where the best human players were paired with
| computers, coining the "centaur" model of human-machine
| cooperation. This is frequently cited in the finance literature,
| where it is recognized that AI-guided human judgement can out-
| perform either humans or machines.
|
| Any math professor knows how to help graduate students
| confidently complete a PhD thesis, or how to humiliate students
| in an oral exam. It's a choice. To accomplish more work than one
| can complete alone, choose the former. This is the arc of human
| evolution: we develop tools to enhance our abilities. We meld
| with an abacus or a slide rule, and it makes us smarter. We learn
| to anticipate computations, like we're playing a musical
| instrument in our heads. Or we pull out a calculator that makes
| us dumber. The role we see for our tools matters.
|
| Programmers who actually write better code using AI know this.
| These HN threads are filled with despair over the poor quality of
| vibe coding. At the same time, Anthropic is successfully coding
| Claude using Claude.
| wizzwizz4 wrote:
| That centaurs can outperform humans or AI systems alone is a
| weaker claim than "these particular AI systems have the
| required properties to be useful for that". Chess engines
| consistently produce strong lines, and _can_ play entire games
| without human assistance: using one does not feel like
| gambling, even if occasionally you can spot a line it can 't.
| LLMs catastrophically fail at iterated tasks unless they're
| closely supervised, and using LLMs does feel like gambling. I
| think you're overgeneralising.
|
| There is definitely a gap in academic tooling, where an
| "association engine" would be very useful for a variety of
| fields (and for encouraging cross-pollination of ideas between
| fields), but I don't think LLMs are anywhere near the frontier
| of what can be accomplished with a given amount of computing
| power. I would expect simpler algorithms operating over more
| explicit ontologies to be much more useful. (The main issue is
| that people haven't made those yet, whereas people _have_ made
| LLMs.) That said, there 's still a lot of credit due to the
| unreasonable effectiveness of literature searches: it only
| usually takes me 10 minutes a day for a couple of days to find
| the appropriate jargon, at which point I gain access to more
| papers than I know what to do with. LLM sessions that
| substitute for literature review tend to take more than 20
| minutes: the main advantage is that people actually _engage_
| with (addictive, gambling-like) LLMs in a way that they don 't
| with (boring, database-like) literature searches.
|
| I think developing the habit of "I'm at a loose end, so I'll
| idly type queries into my literature search engine" would
| produce much better outcomes than developing the habit of "I'm
| at a loose end, so I'll idly type queries into ChatGPT", and
| that's _despite_ the state-of-the-art of literature search
| engines being extremely naive, compared to what we can
| accomplish with modern technology.
| jmalicki wrote:
| We have made those in the 80s. Much was learned about why
| probabilistic stochastic parrots are a far better model.
| wizzwizz4 wrote:
| Those were "let's get experts to manually code every single
| document according to a schema defined in advance".
| Nowadays, we have techniques for automatically-generating
| _explicit_ pseudo-semantic ontology representations from
| large datasets (see, for example, https://openaccess.thecvf
| .com/content_CVPR_2019/papers/Zhang... for image
| classification tasks). Getting a machine learning model to
| identify field-specific heuristics, map conventions from
| one field to another, and then constructing an index that
| allows us to quickly produce a search / proximity metric
| from an arbitrary specification, was not really possible in
| the 80s.
|
| "Throw a massive neural network at it" is an extremely
| inefficient way to get results, and doesn't generalise well
| - for instance, there's no easy way to get online learning
| for a transformer model, whereas that capability just
| _falls out_ of most search engine database systems. (The
| underlying relational database engines had a lot of work
| put in to make online CRUD work reliably, but that work has
| been done now, and we can all build on top of it without a
| second thought.)
| jmalicki wrote:
| Fair enough.
| Syzygies wrote:
| We're in agreement. I understand how much harder it is to
| "think with AI"; the last year of my life has been a brutal
| struggle to figure this out.
|
| I also agree that neural net LLMs are not the inevitable way
| to implement AI. I'm most intrigued by the theoretical
| underpinnings of mathematical proof assistants such as Lean
| 4. Computer scientists understand the word problem for
| strings as undecidable. The word problem for typed trees with
| an intrinsic notion of induction is harder, but constructing
| proofs is finding paths in this tree space. Just as
| mechanical computers failed in base ten while at the same
| time Boole had already developed base two logic, I see these
| efforts merging. Neural nets struggle to simulate recursion;
| for proof assistants recursion is baked in. Stare at these
| tree paths and one sees thought at the atomic level, begging
| to be incorporated into AI. For now the river runs the other
| way, using AI to find proofs. That river will reverse flow.
| wizzwizz4 wrote:
| Lean 4 is not a theoretically-interesting proof assistant.
| If you're interested in such things, look into Rocq (which
| uses CoIC, like Lean, but is more rigorous about it), the
| HOL logic, Isabelle/HOL's automation suite (though Isabelle
| proper is fairly mediocre, apart from being the thing
| everyone's standardised around), Lean-auto
| (https://arxiv.org/abs/2505.14929), and whatever SAT
| solvers are state-of-the-art this week. Like the tools for
| symbolic integration and frequentist statistics, there
| isn't any magic: the power comes from handling enough
| uninteresting special-cases that we get broad coverage.
| (Personally, I think there's still a lot of power being
| left on the table by using overly-general algorithms:
| sledgehammer is used to crack a lot of nuts, even when that
| takes quadratic time or longer.)
|
| While CoIC has recursion "baked in", HOL does not. It turns
| out that we can treat structural recursion as a derived
| property, even over coinductively-defined types. We don't
| even need a notion of ordinals for this! (See
| https://www.tcs.ifi.lmu.de/staff/jasmin-blanchette/card.pdf
| and https://matryoshka-
| project.github.io/pubs/bindings.pdf.)
|
| Lean 2 used HoTT, which _was_ theoretically interesting,
| but not enough was known about HoTT at the time (in
| particular, whether it was a constructive logic - I think
| we have all the pieces for an explicit construction via
| cubical type theory now, but I don 't know that anyone's
| put the pieces together), so that direction has been mostly
| abandoned. I think there's useful work to be done in that
| direction, but with the current state of HoTT pedagogy, I
| doubt I'd ever be able to keep on top of it enough to
| contribute; and with Lean 4 taking so much of the funding,
| I don't think we'll see much work in this direction until
| HoTT is easier to learn.
|
| I still think you're overgeneralising. What actual thing
| does your poetic tree / thought / river analogy correspond
| to?
| wasabi991011 wrote:
| > I'm a mathematician relying heavily on AI as an association
| engine of massive scope, to organize and expand my thoughts.
|
| Can you share more about your architecture & process? Also a
| researcher involved in math research (though not strictly
| speaking a mathematician, but I digress). I've often thought
| about using AI on my notes, but they are messy and even then I
| can't quite figure out what to ask: prioritization, connecting
| ideas, lit search, etc.
|
| I'd love to hear what you do.
| nemo1618 wrote:
| Centaurs are a transient phenomenon. In chess, the era of
| centaur supremacy lasted only about a decade before computers
| alone eclipsed human+computer. The same will be true in every
| other discipline.
|
| You can surf the wave, but sooner or later, the wave will come
| crashing down.
| Centigonal wrote:
| How transient depends on the problem space. In chess,
| centaurs were transient. In architecture or CAD, they have
| been the norm for decades.
| eranation wrote:
| I'm highly worried that you are right. But what gives me hope
| is that people still play chess, I'd argue even more than
| ever. People still buy paper books and vinyl records. People
| still appreciated handwritten greeting cards over printed
| ones, pay extra to listen to live music where the recorded
| one is free and will likely sound much better. People are
| willing to pay an order of magnitude more for a sit in a
| theater for a live play, or pay premium for handmade products
| over their almost impossible to distinguish knock offs.
| lanyard-textile wrote:
| Agreed. But I don't think the time scale will be similar.
|
| Chess is relatively simple in comparison, as complex as it
| is.
| wat10000 wrote:
| On the other hand, chess is not very financially rewarding.
| IBM put some money into it for marketing briefly, but
| that's probably equal to about five minutes of spend from
| the current crop of LLM companies.
| pegasus wrote:
| They are transient only in those rare domains that can be
| fully formalized/specified. Like chess. Anything that depends
| on the messy world of human - world interactions will require
| humans in the loop for translation and verification purposes.
| satvikpendem wrote:
| From a human, to a centaur, to a pegasus, as it were.
| cadamsdotcom wrote:
| This is beautifully written, thank you for writing it.
|
| Typing out solutions to problems was only part of the job
| description because there was no other way to code. Now we have
| a far better way.
| data_maan wrote:
| As mathematically interesting the 10 questions are that the paper
| presents, the paper is --sorry for the harsh language-- garbage
| from the point of view of benchmarking and ML research: Just 10
| question, few descriptive statistics, no interesting points other
| than "can LLMs solve these uncontaminated questions", no long
| bench of LLMs that were evaluated.
|
| The field of AI4Math has so many benchmarks that are well
| executed -- based of the related work section it seems the
| authors are bit familiar with AI4Math at all.
|
| My belief is that this paper is even being discussed solely
| because a Fields Medalist, Martin Hairer, is on it.
| bawolff wrote:
| Paper not about benchmarking or ML research is bad from the
| perspective of benchmarking. Not exactly a shocker.
|
| The authors themselves literally state: "Unlike other proposed
| math research benchmarks (see Section 3), our question list
| should not be considered a benchmark in its current form"
| data_maan wrote:
| On the website https://1stproof.org/#about they claim: "This
| project represents our preliminary efforts to develop an
| objective and realistic methodology for assessing the
| capabilities of AI systems to autonomously solve research-
| level math questions."
|
| Sounds to me to be a benchmark in all but a name. And they
| failed pretty terribly at achieving what they set out to do.
| hiq wrote:
| I'm realizing I don't know if it's currently harder for an LLM
| to: * come up with a formal proof that checks out according to a
| theorem prover * come up with a classical proof that's valid at a
| high-level, with roughly the same correctness as human-written
| papers
|
| Is this known?
| pama wrote:
| The advantage of the formal proof is that the LLM in a loop can
| know that it failed and keep trying.
| Western0 wrote:
| No, this is not a proof because not using Mizar ;-)
| https://mizar.uwb.edu.pl/
| LegionMammal978 wrote:
| Would something be a proof in that sense even if it did use
| Mizar? As far as I can tell, Mizar has no complete reference
| for its language semantics, except for the single closed-source
| implementation. In general, information about the system itself
| (outside of the library) seems very scarce.
| rvz wrote:
| > Conflicts of interest. No funding was received for the design
| or implementation of this project. None of the authors of this
| report was employed by or consulted with AI companies during the
| project, nor will they do so while contributing to it
|
| As it should. Good.
|
| This is a totally independent test not conducted or collaborated
| by any of the AI companies or employees so that no bias is
| introduced at all[0].
|
| [0] Unless the researchers are not disclosing if they have any
| ownership of shares in private AI companies.
| phs wrote:
| I wonder how many of these the authors privately know to be
| false.
___________________________________________________________________
(page generated 2026-02-07 23:00 UTC)