Comment by jboggan

OpenAI: At long last, we have created the Open Problem Strip Miner from classic Terence Tao tweet “Don't Create The Open Problem Strip Miner”.

I don't think the strip mining metaphor is appropriate. Mining is a zero-sum game; if I mine something, nobody else can go and mine the same resources I did. Mathematical problems don't go away when AI finds a Lean proof. They create new opportunities for humans to study the solutions, learn new techniques from them, identify promising directions for future research, discover alternative/more beautiful proofs, and write expositions for other humans.

I hope sincerely hope they don't currently use "proprietary technology" like:

Wolfram Mathematica ($890/yr)

Magma ($2500/yr)

Maple ($680/yr)

COMSOL ($1500,yr)

Matlab ($500+/yr)

Seems like a very strange position to take, in my opinion.

Why does the field of mathematics suddenly now need to be "fair" and give everyone access to the same tools? Has that ever been the case in academics? It's always been a competition for name-recognition, grants, institutions, etc.

Macsyma / Maxima was an MIT developed CAS system back in the 60's that was proprietery until they sold it off to IBM for a tidy sum. Magma actually has free access if you're in the US, otherwise you pay. That's not to mention proprietary MATLAB toolboxes or specialized Stata modules.

Likewise, a lot of the above packages have pretty sweet site-wide deals with R1 universities. If you're at a smaller, foreign one, you're out of luck.

> Tao and others in that group have been strongly and publicly pro AI from the start

Unfortunately being "pro AI" means relinquishing any control over what the AI, or more importantly the company running it, might be doing.

Regarding the advisory group, OpenAI claims to “have drawn on their advice”, which would include not dumping a bunch of AI slop, with the footnote that if they do do that, at least fund the process of digesting it.

At the same time, there's a new note at the bottom of agmai.org stating how they've been in contact with OpenAI about this particular release, and they say that “we consider these discussions constructive, it is ultimately up to the mathematical community to assess the extent to which our recommendations were followed successfully”.

So, what's going on there; is this British English for “they didn't follow anything at all”? Because from my perspective, it looks like they doubled down on the Navier–Stokes approach of trying to maximize PR gain while being as lazy as possible about actually contributing anything back to science, releasing only slop that may or may not be correct and may or may not be straight up plagiarism, as has been the case earlier.

If I were on the AGMAI board, I'd feel terribly exploited when reading that press release, yet their response is modest.

Hairer, if you're reading this: is there any indication whatsoever that AGMAI was anything but a cheap way for OpenAI to science-wash their press release?

Haven't been following this debate closely, but what's the issue with "strip mining open problems"? Surely the supply of interesting mathematical problems is (in theory) infinite?

> stop testing advanced mathematical problems on proprietary models

I don't know but this phrasing comes off as gatekeeping.

That's an absurd idea. The work & knowledge this is trained on is public. You have access to it.

What you didn't make is the AI training process and resulting model. Extremely hard working people built that, and it has value in itself.

Without the AI training process, the model is useless. Otherwise we'd already have been here at GPT-3.

One thing I've wondered about in this respect is what happens if NSA learns 5000 new units of math while the general public learns 4000 new units of math.

This sort of happened at various times in the past, because they hired and/or funded so many mathematicians, and especially before the late 1970s they had many of them working in areas where academic mathematicians weren't working at all, so they were learning more math, or more math that they especially cared about, than the public was. (I was going to write a note here just a few days ago about how NSA has had a "Classified Mathematics Library" for many years.)

For vulnerability scanning, I think the new-capabilities trajectory is good (in the sense of "it will help defenders win") even if governments find ways to get more of it, because there are finitely many bugs and classes of bugs, so at some point more capable models' or longer runs' advantage over less capable models and shorter runs should stop helping them outcompete the less-well-funded defenders, because the defenders will still have learned most of the information that's relevant to achieving successful defenses.

So if NSA gets 5000 units of vulnerability scanning and the public only gets 4000 units, we might still just wipe out all of the pure software vulnerabilities and then go back to worrying about physical supply chain security or side channels or something.

For math, I'm not quite sure! For one thing, there may be things that have no feasibly deployable defense at all even when you understand the underlying mathematics (I'm especially worried about traffic analysis here, because understanding in detail how traffic analysis is done, or how powerful particular techniques are, does not necessarily always or usually make defending against it more convenient or less costly). In a more science fiction scenario, there might also not be any efficient secure cryptographic primitives of some kind, like if it turns out P=NP with reasonably small exponents and reasonably small constant factors.

Based on people I've talked to I'd be really surprised if this was the case, they actually seem to be pretty far behind the ball when it comes to AI use. Which makes sense to me, given the sensitive nature of their data and systems, they don't want to turn on yolo mode and let an agent cook unattended, which is what you need to do to make these discoveries.

I believe it would be a complete failure of the state and frankly downright irresponsible behavior if all the three letter institutions didn't have access to these models and I’m not even a US national nor do I live there. It’s just common sense. Obviously it wouldn’t be public information since it’s national security, but it’s the lowest hanging asymmetric advantage in the history of national security of nations.

It's a grand experiment isn't it? Us senior programmers are pretty good at using AI (or so we think) because we have decades of grinding and problem solving to inform our intuitions. Is that really necessary? The next generation of programmers certainly will not have that level of desk-head interface. Maybe they'll be fine? Maybe the models will get so good it won't matter? Open question.

I imagine the same will be true of AI, but I'll say that in the short term AI is going to make mathematicians better because it solves the breadth problem. Again, I feel like this Barnette conjecture got solved (if it is solved) because of some clever partition function sums which are intellectually tractable but simply too far out of anything I'd seen before (I see the apparition of my GT combinatorics professor intoning gravely that "everyone knows that, Jake, you're an idiot"). Maybe AI will help identify common threads far greater than Google and journal search.

I think if I had ChatGPT when I was 20 and working on this problem for the first time I might not have solved it, but I would have learned every angle and facet of it far more quickly. But then again I would not have spent so many late nights staring at the Országház across the Danube and letting my mind drift and bump against the problem like spilled cargo in the river.

The ways AI can eliminate humanity are trivial obvious and already published. It's just "let the AI control anything of importance and let it spit out slop"

I always got the sense that solutions for significant "unsolved problems in medicine" would be at least 10 years out from the point of total AI dominance in the theoretical sciences. Doing actual experiments is bottlenecked by real-life constraints (organisms are slow to grow and unpredictable, human laws won't let you build a factory to brute-force biology on a million test tube guinea pigs, let alone humans), and the theoretical side of biology is also relatively underdeveloped, to the point that "solve aging" seems as hard to formulate as Navier-Stokes would have been with 15th-century mathematics.

That would be disaster. It would mean the world would not get rid of trump (and similar) by natural causes. Death is the final - and perhaps the only? - equaliser.

A publicly available AI biology wet lab would likely lead to horrific outcomes as people vibe coded virulent pathogens.

If they find a shortcut (like a viral injected cell-dna damage reset) - that would be big. And can you imagine handling the cure for aging, to societies that still produce exponential people?

A cure that you take once and that's it, your body is that age forever? Now, a supplement that you have to keep taking to stay that biological age, that's where the real money is.

extremely obvious you don't understand anything about biology

> I want a jet airplane, but I can't afford one, and all the ones that exist are proprietary.

I guess if you worked together with some people who all put some money into a fund, and by using very modern technologies like 3D printing and modern CAD modelling etc., it should be possible even for private people to build a jet airplane.

The problem rather is that the government does an insane amount of gatekeeping to prevent this from happening (enforcing expensive and time-consuming certifications on airplanes and pilots etc.).

You're talking about an end user not being able to afford a luxury item.

The concern is about elite level researchers no longer being able to move the industry forward in a public way, and leaving potentially all major discoveries in private hands going forward.

Possible worst case scenario in your case, you personally miss out on a luxury item.

Possible worst case scenario in the topic case, an AI company controls the only intelligence that discovers and understands the most powerful tools / physics we know of.

You could theoretically run these (slowly) if they were open weight. ~$10k of DDR4 is enough to hold them. The data itself costs ~0 to replicate.

It's a bit aggravating that I cannot interrogate the session that yielded this result and ask it why and where it got the crucial calculation from, or why it went in that direction. It doesn't even rightly know even if it gives you a legible answer, that doesn't have any correlation with whatever happened under the hood.

Humans are the same way sometimes but I guess there's romance in that. If a human had solved it a la Kekulé and said "it came to me in a dream" I would at least understand that.

Math isn't scientific, none of that is "problematic"

> What exactly are you worried about? OpenAI/etc. gaining too much power?

Yes. They have already shown to have no scruples when it comes to making profit and to have little to no morals.

> If you worry about the government, isn't it better that than rando terrorists?

In my country the largest terrorist attack was almost certainly financed by Iran and caused roughly one hundred deaths. This number pales compared to the thousands who died during the latest, US-backed military coup, a move that relied on a doctrine that the US has never stopped asserting [1].

And those morals I mentioned earlier from AI companies? They do not apply to me because I'm not a US citizen. So no, I do not think the US government is the "seal of quality" you think it is.

[1] https://en.wikipedia.org/wiki/Monroe_Doctrine

The US government has shown, time and time again, that they will always side with large corporations. Having them as the last backstop is not reassuring.

Have you considered the possibility that the AI labs could actually become more powerful than the US government precisely because they control this technology?

Universities, at least, should be given access

> OpenAI/etc. gaining too much power? If they use it, the government can stop them.

Has the government stopped Google and Apple? https://news.ycombinator.com/item?id=49964791

I guess the objection to closed source slurries releasing world-shaking mathematical proofs, from a conservative libertarian standpoint, is that it's inherently dangerous to individuals whenever access to information or technology is concentrated too much in one place, whether that's government, private equity, religions, cults, terrorist cells, or anything else.

That depends on whether the AI-generated mathematics helps with the project of "uncovering the epistemological foundations of the universe".

Which depends on (1) whether there are actual good ideas in it, (2) whether as well as finding the proofs the AIs can explain their ideas in ways humans (and other AIs) can use, and (3) whether the results they prove are ones that really contribute to that rather than being isolated curiosities that don't go anywhere.

I am not expert enough in all these fields, and haven't looked enough at the papers, to assess #1, but in general the way mathematicians have bet is that if you can solve things regarded as important problems you'll usually do so in a way that contains more broadly useful ideas. Differences between how today's AI systems do mathematics and how humans do mathematics might make that less true when it's an AI that solves the problem, but I would still bet that way. I'd be surprised if OpenAI's big math dump didn't turn out to contain some ideas, and connections between ideas, that humans find useful.

At the moment the AIs are worse than good humans at #2. (But some humans are also really bad at #2, including some humans who are very good at proving theorems.) It looks to me as if they're getting better, and I would expect them to continue to do so. I also suspect (but this is only guesswork) that today's publicly-available frontier AIs may be able to answer questions along the lines of "please take a look at this AI-written paper, and tell me what key new ideas it contains and how they relate to other things in the field" well enough to be useful to human mathematicians. (Even when the paper itself was written by a proprietary AI that no one outside OpenAI or Anthropic or Hypothetical New AI Mathematics Lab has access to.)

As for #3, that's always been something of a crapshoot. A lot of mathematicians' effort goes into proving things that approximately no one ever reads or builds on, just as a lot of industrial R&D goes into trying things that don't turn out to make good products. The recent OpenAI dump contains things that sure seem like important building blocks for future mathematics (e.g., the "quasi-Riemann-Hypothesis" thing) but it's hard to know for sure and also hard to know whether, if they do prove things that turn out to be useful, it's only because they've read the human-written literature and aimed at things human beings have said seem likely to be useful.

None of this seems to me like "adding AI here does nothing". Whether what AIs are doing to mathematics at the moment is good on balance is highly debatable, of course, but it's a matter of trading off costs and benefits, rather than there being costs and no benefits.

You should try asking an LLM to look for previous papers using similar ideas. The current/frontier generation of math AI is unfortunately very bad at citing the relevant literature for techniques its using.

I asked GPT here: https://chatgpt.com/share/6ac5fd7d-0390-83ed-a02a-6d80fc64f6... and it says:

> the exact Barnette argument appears quite novel, but nearly every ingredient in its cancellation trick has a recognizable ancestor.

> The closest precedent is much closer than I expected: in fully packed O(n) loop models, people have been assigning complex phases to the two orientations of a loop and making them cancel for decades. At n=0, the phases are literally +I and -I. And the n->0 limit has specifically been used to extract Hamiltonian cycles/walks.

You can judge better than me. But it's definitely worth it having a research assistant AI with you when reading these papers.

BTW, reading your last paragraph reminds me of how Lee Sedol felt after move 37.

Complex roots and annihilating terms -- is it something like the derivation of Fourier / Laplace transform?

WOW

Why would the trick have any "origins", isn't this model creating new techniques never before seen or imagined?

From my current understanding (and a lot of theoretical physics I'm having to Google because the sentences I'm reading from Fable's analysis are so bizarre I think they are hallucinations) there are possibly 3 neat symbolic tricks borrowed from theoretical physics that make the heart of this proof. Forgive me for posting LLM output but I find this darkly hilarious:

"it's a matrix-tree cancellation wearing Kasteleyn's planar signs, run as a Witten index over Penrose-lineage states, evaluated as a fugacity-zero loop gas in an infinitesimal magnetic field — and the reason it reads like physics is that every one of those tools was built for partition functions"

I thought this was pure slop when I read it but there are some clear analogues in these other areas of physics, really neat computational tricks, and a very interesting paper by Penrose calculating Tait colorings I never knew about previously (extremely relevant, actually related to a separate approach I had once taken on this problem). The problem is that the paper isn't saying "aha, we were inspired by the related problems of pairing excited states and creating spanning trees out of cancelled coefficients" it just defines the function apropos of nothing. Which is kind of like the Jacobian counterexample in that it works but doesn't really explain how exactly it got there.

I really think the load-bearing concept here is "prior work". If prior work is considered papers on this problem or graph theory, yes this has one huge subjectively unintuitive logical leap. If "prior work" is the entire corpus of neat computational tricks that physicists derived to make their equations spit out something other than zero or infinity, maybe it's not so crazy?

My favorite thing about your story is that you wrestled (enjoyably, it sounds) with a known problem for decades, but are finding fulfillment in an open ended problem that is exercising creativity about both problem and solution.

IMO that’s where AI is going: as soon as a problem can be formulated clearly enough, AI will trounce us humans. I have yet to see evidence that it can decide what problems are important at a remotely human level.

The process is often as valuable as the end result. Sure, you didn't crack the problem, but you gained enormous value in the process. I consider that a win.

If you wrote down any of your thoughts on the open Internet you are probably in some small - or possibly large, unattributed way, responsible for this result being possible.

Where can I learn more about your upcoming product?

I think this is going to come down to personal philosophy and religion. And having a strong grounding in history to help us all through whatever changes we are rapidly living through.

[dead]

https://www.reddit.com/r/accelerate/comments/1wzqe8d/interes...

If I didn't live in Budapest already I'd be questioning the authenticity of this retelling. However I've seen so many crazy things there that I find it very easy to believe.

Indeed!

I've been mentoring (or so I'd like to think) a very bright undergraduate mathematician, in fact he was the one who pointed out the final irreducible flaw in my proof last summer. And I am extremely curious to see what he does and if he even finishes his degree in mathematics. He had already expressed to me some dismay that his summer undergrad research program with several Ivy-league math majors got blown out of the water by a few hours of a frontier model. It's making everyone question what the future will look like and what education and training and certification will even look like.

But the future belongs to those who show up. Maybe this is the beginning of a mass democratization of scientific and math research, maybe we are going back to the gentleman-scholar model of amateur researchers and Twitter will be the new Journal of the Royal Society.

This experience of alienation is a social consequence of the mechanization and automation of mathematics as intellectual and creative work. There is no author or thinker behind the creation of the proof, only the practical result. It's the same process as the industrial revolution, but applied to the intellect and mental work, where factories and machines replaced manual craft, devaluing the community, culture and humanity around the work.

In programming we've been dealing this for a while. You see some weird code that doesn't make sense, maybe it's a lack of your understanding or maybe the code is bad, but you can't ask the author anymore since it's an AI.

Beautifully put.

> It's just another enigma but one that is far more unknowable than the original problem.

You just made my day, beautifully said. Thank you Sir, for all your thoughts expressed in this thread. You put an human story behind the #180 number.

In this case, once the model is released anyone in the world will be able to go to https://chatgpt.com/ and talk with that model.

First sentence of the article: We’re releasing a broad range of new mathematical results produced by an internal frontier model.

You are really excelling in this thread. Thank you for your insights and wisdom, I'm really enjoying everything you are contributing.

Lol it should be, but it doesn't seem complete. Line 49 just says "sorry"

/-- Cubic bipartite three-vertex-connected plane graphs have a Hamiltonian cycle. -/ def MainStatement : Prop := ∀ (V : Type u) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], G.IsRegularOfDegree 3 → G.IsBipartite → Planar G → ThreeVertexConnected G → HasHamiltonianCycle G

theorem main : MainStatement.{u} := by sorry

We only need smart people with valuable opinions here, no one else is allowed.