danabramov

4 ms·

1.
by danabramov 7d ago
>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 res
2.
by danabramov 7d ago
I'm not sure it is trivially automatable with today's models since they get "carried away" too much, and I'm not sure there's a good way to prevent the supervisor from drifting. But I would like somebody to att
3.
by danabramov 7d ago
I agree, that's a clearer way to apply it. I guess I see myself more as a guy who, with some effort, managed to scan a few pages of the codex and posted it on the internet. Now, to be consistent, would you say that you'd be equall
4.
by danabramov 7d ago
What does "taking credit" even mean here? I am not saying that I contributed to the mathematical work in the proof. I am simply disagreeing with you that the process is fair to describe as plain continue-shotting. You saying &quot
5.
by danabramov 7d ago
I invite you to continue-shot this result. I haven’t been able to do that with the current models in a separate control session. It might be possible to plainly continue-shot it with more powerful models in the future. I agree that whatever
6.
by danabramov 7d ago
What is the value that I am extracting? The alien in the analogy is the corpus of knowledge that’s newly reachable via LLMs.
7.
by danabramov 7d ago
Imagine we discover an alien spaceship, and inside it, a codex. Decyphering the codex tells us a bunch of solutions to alien mathematics, which is remarkably similar to ours and has compatible foundations, but way more convoluted in the act
8.
by danabramov 7d ago
If there is consensus on how to attribute credit for LLM-solved human-steered (with no mathematical human input) proofs, I am happy to follow that consensus. Do you have a concrete alternative recommendation? What should I change?
9.
by danabramov 7d ago
>I interrogate it, I ask it to back up and replace its jargon, and I force it to be accountable 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 (asi
10.
by danabramov 7d ago
What do you want me to call it? I'm fine calling it your result if you want.
11.
by danabramov 7d ago
Is a YouTuber speedrunning a game by exploiting an integer overflow bug suggesting that gaming has no value? No, they're just having fun with the medium. To answer directly: I think understanding is the primary value. And I have reas
12.
by danabramov 7d ago
I was not "mindlessly continue-shotting". The way you describe it is literally the same as "one-shotting" and, as I explained in the article, it simply doesn't work. You are welcome to try it yourself on this proble
13.
by danabramov 7d ago
I’ve replied to this here: https://news.ycombinator.com/item?id=49762433
14.
by danabramov 7d ago
I may be wrong here but my impression is that surreal numbers in general are kind of a niche area that hasn’t enjoyed a ton of interest. Additionally, this specific conjecture did not have any “prizes” attached to it and was not on any list
15.
by danabramov 8d ago
OK this is probably not quite what you meant but I'll shoot: I highly recommend Terence Tao's Analysis textbook (which now also has a Lean counterpart on GitHub). You can skip Chapter 1 (it sets up the motivation but I couldn&#x
16.
by danabramov 8d ago
Perhaps you and I read this document differently. This is not a “famous problem”, I am not a “major AI company”, and I am genuinely interested in increasing mathematical understanding. To the last point, here is a comment from a mathematici
17.
by danabramov 8d ago
What is the problem with saying “nothing” to mean “empty set” in an informal explanation? If you put apples between two bags, and the right bag is empty, it’s reasonable to say “nothing” accurately describes the contents of the right bag. I
18.
by danabramov 8d ago
Thank you for writing a detailed explanation! I've slightly edited mine to explain the infinity jump. Yours is, of course, much more detailed. For the infinitesimal number, I think it makes more sense to use {0}|{1,1/2,1/4,1&
19.
by danabramov 8d ago
I'm a little tired from the project so not eager to jump back into it right away. But yes, I'd love for useful pieces to make their way into https://github.com/vihdzp/combinatorial-games . Violeta, who maintai
20.
by danabramov 8d ago
LLM didn't write anything in my post; these are all my words and my choices. Conway himself described surreal generation in short like this in ONAG: > We may say that Cantor was only interested in moving ever rightwards, whereas De
21.
by danabramov 8d ago
I try to address this in the post explicitly in a few places. Primarily I thought of this as a sort of "epistemic performance art project", maybe similar to playing Elden Ring blindfolded having never played it before, or speedrun
22.
by danabramov 8d ago
I've confirmed with the mathematicians working in that field that this is a new result.
23.
by danabramov 8d ago
If I may offer an analogy, what I tried to do is essentially reporting a bug after having a failing unit test that exercises the public API, without looking into the black box of internals.
24.
by danabramov 8d ago
Hah, very interesting question! Let me first clarify my relationship with mathematics. I think of myself as "an awestruck observer from a distance". I find some parts that I understand beautiful, and I have also tried to understan
25.
by danabramov 8d ago
It's new but there is actually a registry now: https://palomar-registry.org/
26.
by danabramov 8d ago
Just saying (as an author) I don't believe that LLMs have conscious experiences, but the word "mood" was a good languagespace anchor for the kind of information I wanted to get out of the LLM at the time.
27.
by danabramov 8d ago
I see, we don't seem to disagree much. While Lean is tightening things up after the recent LLM-driven hacks, I agree that bugs are possible. Although usually code that exploits them is obviously aggressive and is deliberately using the
28.
by danabramov 8d ago
What is your point, exactly? Increasing number of people working in and around mathematics are relying on Lean kernel's correctness. That's kind of the point of tools like Lean. Why is it a problem for me to publish a result that
29.
by danabramov 8d ago
Yeah it's a pretty tough question! I've resisted doing that until I had a relatively high certainty that their published results contained minor mistakes, which I assumed they would want to know about. I've also been explicit
30.
by danabramov 8d ago
It's more that surreal numbers already include infinities like ω, ω + 1, and so on, so "inf" felt like a concept I want to avoid. The actual description is set-theoretic and uses empty sets there ("nothing to the left&qu

More ›