Posted by m-hodges 4 days ago
> And the control column confirms the resonance-necessity conjecture empirically: break the skeleton alignment and the joint kernel dies at the constrained window, exactly as the transversality heuristic predicted.
> The den has air in it.
> Drift fuel exists.
You can so easily imagine this shit being read in a 90s slam poetry coffeehouse. Trust me I was there
You are right, maybe some humanities classes would've helped or I'm just wired this way.
(Of course, prose is sort of like a superset of poetry - it's not a hard dividing line. You may find especially poetic lines in your favorite longform works, especially in good fiction books.)
I do think that many English teachers do a poor job of encouraging a love, or even understanding, of poetry. One of my highschool teachers was in love almost with categorizing the forms of poetry - sonnets and sestets and villanelles, and seemed to think that if we learned the rules about what lines had to rhyme or which syllables to stress, we'd enjoy poetry. I hated it! But then the next year, even against this backdrop of learned avoidance, my teacher was so in love with the ability of poetry to communicate - the unfolding of a few words into meaning like a flower in bloom - something clicked. He focused almost not at all on the structure of poetry, but rather on finding works that spoke to you. I'm still not a lover of poetry, even now, but I have poems I appreciate.
Either I really misunderstood high school English classes or this is what poems have always been known to do.
I'm not a mathematician. Can someone explain to me how this approach gets you beyond the rational numbers?
Also, this was formatted as a blockquote, but as far as I can see, this blog post is the only instance of this formulation online.
Agreed, and it's a wonderful piece of art. I look forward to seeing the actual publication and reaction from the math community.
[1] https://eps.leeds.ac.uk/maths/staff/4058/dr-vincenzo-l-manto...
Edit: Another depressing fact is that he generously paid to LLM megacorps while piggy backing on human help for free and in the end calls the proof his or LLM's.
To answer directly: I think understanding is the primary value. And I have reasons to hope that my "work" here can ultimately contribute to a better understanding: https://news.ycombinator.com/item?id=49761718. However, there are also other reasons to do things than producing value. You can do things for fun, to show they're possible, to ask meta questions about the field.
Regarding calling the proof "mine", I've replied to that here: https://news.ycombinator.com/item?id=49755885.
I read your comment and my edit was inspired by it. Your article only mentions nameless mathematicians, without really giving credit.
I explicitly give credit to the papers the proof builds upon. Quoting from the article:
>The proof was only possible thanks to the many existing results from [References](https://gaearon.github.io/conway-refinement/#/references). In particular, [A factorisation theory for generalised power series and omnific integers](https://doi.org/10.1016/j.aim.2024.109513) by S. L’Innocente and V. Mantova has played a crucial role in the proof.
The project README (https://github.com/gaearon/conway-refinement) also states:
>Over the years, Berarducci, Pitteloud, Pommersheim and Shahriari, and L'Innocente and Mantova developed increasingly strong results about exactly that. This proof builds on all of that work and claims to finish the refinement conjecture.
It includes the same list of references: https://github.com/gaearon/conway-refinement#references
Regarding who I've talked to over email, I wasn't sure I want to "out" them explicitly in the article due to the article's likely polarizing nature, but, since he already engaged in this thread, I can confirm that this person was Prof. Mantova (who is a co-author of the primary paper that the result I published rests upon, and who I did explicitly credit in the text of the article and in the references).
You can read Prof. Mantova's own reflection here: https://news.ycombinator.com/item?id=49761718
I have not had an extended conversation with anyone else.
>Following your analogy it is not a very fair game if it allows winning for those having access to latest exploits. Playing against skiddies who bought the hack kind of ruins it.
You misunderstood the point of my analogy. The point was not that it is a game in which you "win" or "lose" and thus I have "won" or something like that.
The point was that "obtaining a true proof without understanding it" doesn't imply "understanding has no value" any more than "completing a game in an unintended way" implies "playing has no value". You stated a false implication. That false implication is what I am highlighting with the analogy. Understanding has a societal value; doing something weird for the fun of it has value to the person doing it; sometimes people do things with no value at all, and that's okay too. Each individual act is not a statement about what kinds of things have value.
Personally, I do not see mathematics as a game of "win" and "lose". If the broad value is primarily in understanding (which I think is correct), then my "contribution" doesn't make much dent in that. However, it might, as Prof. Mantova mentions, help show the way to an actually useful proof that improves collective understanding. That would please me beyond merely having had fun. In any case, I've enjoyed the experience of it in part due to the absurdity of it. Maybe it requires a certain kind of sense of humor.
Regarding the models, as far as I know, all of the models I have used are currently broadly available. Yes, they require subscriptions so access is not democratized yet. There's nothing I can do about that. I think it's unreasonable to require that someone playing around with LLM's must use the inferior free models.
And about the "value" I think we picked different meanings for this word:
For me for something to have value means it can be used for something else. In this sense you cannot pick what has value. There are people with deeper understanding of the subject than yours yet they were unable to use it to come up with a proof. You had no understanding but you had succeeded. Therefore understanding in this particular case had no value. You did not have to state it, it flows as a natural conclusion.
You can also say that being good at chess or catching all the pokemon has a value for you or for some society. This is true but it has to do with self-actualization rather than dealing with circumstances.
I also do not see how you can say you did not win anything. This proof will be a great addition to your portfolio which in turn will serve as a leverage while searching for your next job, even if it never comes up explicitly. It is a dream for some folks to be talked about on hacker-news. Good for you that you can treat is as if it was nothing, and I do not mean it as an irony.
I do that too when working on software. Here, I did a little bit of that, but it is much harder when I have almost no domain knowledge (aside from understanding the statement of the conjecture), since at each point the LLM might trick me anyway, and it would probably take me a year to understand the concepts enough to tell when what it's saying doesn't make sense.
>Even just keeping the Lean more up to date would have likely saved tokens
That's the conclusion I came to by the final week! But don't underestimate how much Lean needed to be written in the first place to even "catch up" with the reference papers. I had no option to keep it up to date when I started.
> Although the current generation of models is trained to complete tasks rather than to enrich our understanding, and today’s AI companies are misaligned with the goals of the mathematical community, I hope that with time we’ll find ways to use these tools in harmony with human research.
while citing "A Severe Misalignment of AI in Mathematics" [1], which condemns exactly the thing he is doing himself: Mindlessly producing theorems without a corresponding human understanding of the underlying proofs.
The happy case here is that my obtuse proof leads to a concise and illuminating mathematical proof, which is exactly my hope for the endeavour. I think this could then be a positive example of AI/human and amateur/professional collaboration.
What would a positive example look like to you? What do you think the manifesto argues for?
Positive example: Someone is 1) independently interested in a particular conjecture, 2) he lets an LLM prove and explain it, 3) he ends up fully understanding the LLM proof and is then able to phrase it in his own words.
Edit I apologize to Dan Abramov for venting my frustrations about things outside of either of our control and unfairly using him as a punching bag. He seems to be an intelligent person and I hope he continues learning mathematics using whatever tools he sees fit, including AI. It was wrong of me to do this and I will take a break from this website for one week.
With all the talk of mathematicians possibly being obsolete, I'm wondering where the future conjectures that future LLMs would prove might come from.
My read on the current sitch is that the drama is more around the humans behind the LLMs, like the OpenAi *people*, who are dishonest, thieving, technocrats, stealing human mathematicians work and claiming credit for it. Since the LLMs are only trained on finite amounts of data on the internet I don't think anyone expects them to replace mathematicians in a serious way. But surely the field is changing dramatically, people will adapt.