nilkn · HackerLangs

8 часов назадdiscuss

We're talking past each other for some reason. I'm not "unhappy" with anything. I just pointed out that (1) a result like this requires peer review by a professional human mathematician, which fundamentally bottlenecks progress in a pretty severe way; (2) such review would not be necessary if it were accompanied by a formal Lean artifact; (3) you can have both a formal proof and an informal proof together (one does not rule out the other); (4) searching for proofs formally first, then translating successful auto-verified proofs into natural language, is the most scalable approach in the near future for AI mathematics; (5) AI conjecturers would likely benefit from the results of (4) for making large leaps and connections, which can then scale into formal proofs for verification, which then feed back into the same loop ...; (6) humans guide this process through taste, judgment, and their own intuition, likely often intervening to ensure that the loop is aligned and producing a body of conceptual informal mathematics that is valuable to humanity.

nilkn

9 часов назадdiscuss

You are assuming that the latter, once autonomously discovered and verified at scale, could not simply be translated into the former, also perhaps autonomously at scale (or otherwise selectively as determined by human interest, taste, and relevance).

nilkn

9 часов назадdiscuss

I disagree. It's the only way to scale AI mathematics far beyond human mathematics. Any interesting verified result would, obviously, be rewritten back into natural language for human understanding and consumption (as well as potentially for the benefit of AI conjecturers too). You are falsely assuming that advances in formal mathematics would not feed back into similar (potentially massive) advances into informal mathematics, and I think that's simply wrong. We're just at the very, very beginning of that curve.

I think this is, in fact, inevitable. It's the exact same RL loop that allowed AlphaGo to vastly exceed the world's top human players. You can theoretically RL formal proof techniques vastly beyond human capability by removing the need for any human review for correctness. It is completely reasonable to assume that "informalization" will become a real sub-field of mathematics in the near future.

nilkn

9 часов назадdiscuss

Nah, if it produced the proof in Lean which is automatically verified to be correct, you could then just write a natural language version of the proof to accompany it (often using AI to do that part too). That's becoming the standard for AI math these days. Generating purely informal natural language proofs via AI is fundamentally bottlenecked by requiring rare professional mathematician review on every single candidate output proof.

nilkn

9 часов назадdiscuss

Formal methods post-AI are completely different than formal methods pre-AI. There are multiple companies (Axiom, Harmonic, Logical Intelligence, etc.) developing neural theorem provers that do exactly what the commenter above mentioned, and it works.

nilkn

10 часов назадdiscuss

> At no point did anyone think to explain that we were measuring the areas under curves, or their rates of change

That's odd. Odd enough that I'm not sure I even believe you. It might be more likely that you weren't interested at that time and didn't really digest what you were being taught. I don't think I've ever heard of high school students being taught calculus with zero mention of areas under curves or rates of change.

nilkn

10 часов назадdiscuss

Since this isn't in Lean and it's extremely easy for something like this to contain a subtle mistake, I think I'd prefer this be announced by a professional mathematician. The proof appears relatively short and elementary (not to be confused with easy -- just not using any advanced or modern machinery) so it shouldn't take long for the mathematics community to do a peer review. Without that, you could easily crank out hundreds or thousands of PDFs like this that all look plausible and are beyond the ability of a gifted amateur to review.

nilkn

14 часов назадdiscuss

You were certainly not switching back-and-forth between Fable (a model available to the public generally only since July 1) and Codex for the last several months.

nilkn

15 часов назадdiscuss

Hard-to-predict memory performance over time is enough of a reason to never seriously use Haskell in production. These days, if you really like the type system, just use Rust: most of the type system benefits, vastly easier to predict its performance and memory usage. Space leaks in Haskell are no joke.

That said, I'm convinced that language choice is pretty much irrelevant, outside of avoiding particularly horrible languages for production, of which Haskell is one of the biggest examples.

nilkn

вчераdiscuss

This is not what I was expecting, and there's no way this design lasts very long.

It needs to just have one mode that can do anything. That's it. The only choice to make, really, is whether agentic tasks run locally on your machine or in a VM on a shared cloud.

nilkn

вчераdiscuss

I'm not sure how meaningful this is. Fable only just recently become more broadly available, and GPT-5.6 is launching broadly today.

nilkn

вчераdiscuss

Codex has arguably been better than Claude Code for months now, but it's flown under the radar because it just didn't capture the same viral marketing effect and OpenAI in general has had more optics / PR issues than Anthropic amongst the online developer crowd. I use the word "better" not in the sense that the underlying GPT models are fundamentally smarter or more intelligent, but rather that as a product Codex is just simpler, cheaper, and abundantly reliable and low-drama.

nilkn

11 дней назадdiscuss

There's a lot of really important software out there where being able to easily verify effect-free core logic would certainly be very useful. An e-commerce web app is not a good example. Anything safety-critical -- aerospace, defense, medical devices, power generation, industrial machines -- already requires a certification process. Auto-generating proof evidence as part of the cert process (which generally requires a rigorous spec anyway) in the near future seems like a no brainer.

nilkn

14 дней назадdiscuss

So the frontier will just decisively shift to open Chinese models in the near future, and once that happens, there will be no catching up.

nilkn

16 дней назадdiscuss

That's because the company likely doesn't view it as a mistake. The executives did their job: they tried something the company likely considered reasonable (or even strategically necessary) and pivoted based on results. At the executive level, that's not considered a blunder. What counts as a blunder would be (1) being too cautious to try a change, then falling behind your competitors if that change turned out to be critical or successful; (2) attempting at change, seeing that it didn't work, and refusing to pivot or falling prey to the sunk cost fallacy.

nilkn

24 дня назадdiscuss

I use Windows on my home PC simply because it's such a versatile setup thanks to native GPU support, game support, and WSL2. It feels like I can do almost everything on one machine with little to no compromise. If I didn't care about games I'd probably load Linux onto it, but WSL2 gets me most of what I want from both worlds without needing to do that.

nilkn

29 дней назадdiscuss

I'm not sure why we would assume that AI-generated or AI-assisted mathematics would never amount to anything useful in the real world. I would expect the opposite: the usefulness and explanatory power of mathematics has been riding an exponential over the last several centuries.

Maybe I didn't do a good job explaining it, but the rest of my prior comment was about connecting AI-generated results back into human-style thinking. Inevitably, in the far future, it's not unreasonable to assume the world will be dominated by synthetic robots controlled by artificial intelligence, and there will indeed be a point where AI builds not just bridges but vast planetary, interplanetary, and space-based infrastructure projects beyond the ability of our current civilization. At that point, mathematics may permanently move beyond the grasp of the human species. You can't teach a dog general relativity. Surely, there are truths in mathematics (and possibly physics) you cannot teach a human. Not to digress, but for me, this kind of threshold is what a term like "superintelligence" means -- the point where an intelligence is discovering truths that cannot be taught back to humans because we're not smart enough. So far, our contact with this kind of intelligence has been limited to one-off, highly specialized cases (like chess) that have little grand implication for civilization, but that won't always be the case.

But, for today and probably at least our lifetime, to make them useful major AI advances in math will need to be "compressed" back into the specific network and "towers" of concepts and abstractions that human minds specifically can understand and intuit about. So I think both directions of formalization are equally important: translating natural language statements (theorems, lemmas, etc.) faithfully into Lean and letting a theorem prover run and decoding a dense Lean proof back into natural language (which, in some ways, is the more creative and open-ended problem -- there is no one right answer).

nilkn

29 дней назадdiscuss

An inscrutable 1000-page Lean proof may have low transmissibility amongst humans, yet extremely high transmissibility amongst AI mathematicians.

Probably AI mathematics needs a specially constructed or trained translation or compression system (likely also an AI system) that helps transmit dense Lean proofs back into human-style thinking. We may even see an entire field develop around creating human-comprehensible compressions of vast formal breakthroughs in mathematics. Such an activity would almost certainly be both art and science -- there's some objectivity in that certain abstractions or definitions inherently cover more ground more efficiently, yet there's also a deep creativity and artistry in finding compressions that are adapted to the specific 3+1D spatiotemporal intuition of the human mind. Perhaps with time this will keep a lot of the originality and creativity of research mathematics alive -- maybe with that work having even more centrality than it does today.

Instead of seeing this all as a loss of beauty in mathematics, I choose to see it as the beginning of a new age, which will bring entirely new problems to solve, yet also accelerate discovery at an exponential rate.

nilkn

29 дней назадdiscuss

I don't think Terence Tao sold out. However, just looking at it from OpenAI's perspective, this kind of advertising is almost certainly worth at least one order of magnitude more than $3M to the company.

nilkn

в прошлом месяцеdiscuss

I bought it on launch day, and I still use it at least a couple times a week. I also pretty much always take it with me when I travel (along with my MBP). Frankly, I'd use it even more, but because it's a fairly anti-social device I prefer to use it only when I have meaningful alone time. If I were living alone by myself, I imagine it could be a daily device for me.

My main use cases are Mac Virtual Display, movies/entertainment, PS5 gaming [0], casual browsing, and -- most surprisingly -- reading. The first few are pretty self-explanatory, but reading is one of my favorite unexpected niche use cases. It's really nice having a floating book (via Apple Books) perfectly positioned at eye height in front of you in your favorite virtual environment, listening to music of your choice. This use case didn't really take off for me until the recent dual knit band fixed the comfort issue. I dabbled with reading in the Vision Pro before but the comfort level just wasn't quite there yet. The new band is good enough to make this one of my favorite ways to read today.

[0] I use the Portal app for this. It lets you stream PS5 games into a gigantic screen inside the Vision Pro. I combine it with a Dolby Atmos surround sound speaker setup in our upstairs game room. It's truly a stunning experience. The only reason I wouldn't declare this the gold standard way to play games is because it currently relies on WiFi streaming, which introduces some input lag. The lag tends not to be an issue with the games that I play, but it's enough that you wouldn't play competitive twitch shooters with it. If Apple had just allowed you to plug in an external device via HDMI, this would hands down be the most impressive gaming experience out there. I'm personally very sensitive to input lag thanks to years of low-latency PC gaming, but I know not everybody is. If you're not, you may be even more impressed by it than me.

comments