I switched from vi readline mode to emacs recently primarily for Ctrl-r and Alt-. (insert the argument from the last command). I love how interactive they feel.
You can accomplish the same things in vi editing mode (with ? and !!) but they’re not as interactive.
No one is saying you can’t solve puzzles that have already been solved. If you love solving puzzles, then whether it has been solved doesn’t seem all that important.
> That said, if slowing this down were possible, I think it would have happened by now. Maybe he’s hoping the OAI/HF incident becomes something the industry can rally around, but it won’t.
I disagree with this and I think the reason is well captured here:
> The idea of pausing or slowing AI has been floated as far back as 2023, and I think it made little sense back then... The AI models of those days were not powerful enough to act as agents in the world in any coherent way, and were not capable of significant deception, manipulation, cheating, or cyberattacks... Today, however, the picture is totally different.
Hard disagree, to the point where I'm not sure there's not some confusion at play here.
I find using indices and summations generally confusing and hard to read/follow/understand. To me, it's so much simpler to draw out the computational graph, derive the gradient with a single element (so I'm in agreement with you guys here?), see how that applies the same to every element the same, then scale up to the vectorized/matrix version.
> and you need to memorize a bunch of new rules to apply it
There's nothing to memorize though..?
Is there something called "matrix calculus" that's different than just drawing the computational graph and deriving the gradient in the way I described..?
I don’t see why it makes a meaningful difference if a human solves a math problem versus AI - it seems like the same amount of understanding will come out in the end. Either the understanding will come from humans arriving at the proof in the former case, or the understanding will come from humans understanding the proof that the AI came up with in the latter.
Probably an AI-written Lean proof is very different to how a human would write it, and some may say it's more like mathy neuralese. For sure it works but it is not human-friendly and needs to be transformed into something more readable and digestible to be able to extract insights from it.
Not that different from when trying to read an out-of-control vibe coded codebases, or an sloppy AI long email that someone may send you at 9 AM.
Tao has a spiel in his recent interview with Dwarkesh where he says that AIs are very good at explaining things - so just have the AI explain the proof in a human-friendly way.
For sure, but this was supposedly ~18 million dollars of compute, afaik 100 pages paper / lean proof and only god knows how many bytes of chat interactions + thought traces. Scale matters.
I bet it can be decomposed quite nicely though. At the top level, there are probably only like five steps. Dig as deep as you want into any of those steps (i.e. engineering).
Because the problem has almost no value unto itself. The clay statement of navier stokes is not relevant to how CFD is done in practice.
It's about what is non verifiable versus verifiable. The same way it produces "slop" code (which, if you give it test cases, will be 100% correct), it also produces "slop" math.
Code that serves a business function, it's ok if its slop. Math that serves directly a business function also can be slop.
But most open problems are not directly for a particular usecase. People agree widely to attack it due to the perceived possibility of encountering useful mathematical objects along the way, that will then expand the world's mathematical toolset. This is not something that you can easily express in a verifier, and is thus something that is hard to force an LLM system to do.
You are right in that understanding it retrospectively is possible, but that is not going to be as useful as the desired "elegant" objects that expand and unify mathematics. You can't represent these concepts in verifiers.
Again, if you let AI rip at something like say "beat shannon capacity" and suppose it comes up with MIMO as paulraj did, great! It's useful and you can retrospectively understand it, say by expanding shannon to multiple dimensions, as foschini and telatar did. But most math problems are not in that category.
The question then is, if AI is really good at this type of math, how much of the existing mathematical community+process is necessary? I think it will still be necessary, just maybe in fewer cases. Wherever the primary purpose of the math is in a domain and that domain has a verifiable target, we can directly optimise it to that verifiable target in-domain rather than reach for the mathematical community. How well will this work? We'll see. It's not clear if it's even possible to represent most problems this way.
Props to D for having such a simple implementation of fexprs[1].
The downside compared to macros I think is that, as argument expressions become lambdas, it becomes harder to manipulate them. Check the cond example which needs two fexprs, whereas one macro could do it.
Not sure about D, but if it were lisp, even lambdas could be manipulated as lists. Macro args not having the lambda wrapping just seems simpler.
Or you could wrap arguments in lambdas (anonymous functions) for eagerly-evaluted languages. Lisp unfortunately has a bulky syntax for lambdas, compared to something like Smalltalk. Of course, you can fix this with reader macros in Common Lisp (but no one does). Clojure has a shorter syntax I believe as well: #().
Unless laziness is pervasive (I guess, no knowledge about GHC internals), you basically have an FEXPR (https://en.wikipedia.org/wiki/Fexpr) which was replaced by macros for good reasons.
Technical Support Specialist with 5+ years software engineering background. Diagnosing and resolving technical issues, communicating clearly with both technical and non-technical users. Background includes API debugging, cloud infrastructure (AWS), Python, and data systems.
Currently pursuing customer/technical support roles. Open to support engineering roles.
You can accomplish the same things in vi editing mode (with ? and !!) but they’re not as interactive.
reply