Oh I remember this from the classic SO post, but it was just presented as a funny trick. I never realized that it solves the issue mentioned in the article and there is a legitimate use-case for post-decrement in the comparison itself.
There is nothing clearer about your way unless someone is just starting with C.
'while (i--)k is a shortcut, which might seem terse when one first encounters it, it is a well-established and trivial to understand construct. On the other hand, your embellishment only adds pointless friction when reading the code.
if `i` ever gets modified inside the loop, and skips 0 (e.g., got decremented twice when it is at 1), then you might end up with an infinite loop?
Usually, this won't happen of course, but because `i` is not declared inside a for-loop, it must have been declared outside, and thus might even look like a regular variable that could be used by some "clever" coding to multipurpose it!
In any case, it's a niche worry i have, so i usually don't do it if i know there's a for loop that would do.
I don't think it's too clever at all. Notably it works with both signed and unsigned i. Frankly if I see anyone doing anything other than this, they're wrong.
The part I like is starting from the count rather than count-1. If n is 0, `i --> 0` never enters. Do `size_t i = n - 1` and a zero-length array wraps to SIZE_MAX first, which is the case that actually runs off the front.
> It's June 16, 1987. Ted Uhlemann ("iczer") plugs an Apple IIe's 300-baud[1] modem into a phone line his mother had just given him for his birthday, running Magic City Micro-BBS (written in Applesoft BASIC). He names it SDF-1 after his favorite anime
Dude was into anime in 1987?? Truly ahead of his time.
Robotech (the americanized version of Macross and some other anime) was broadcast on regular TV (local stations) in 1985. I watched the entire series (I was 12 at the time) with my jaw on the floor. Already The Last Unicorn had shown us what Japanese animation was capable of, and Robotech brought things up a notch (not in terms of animation quality, but in terms of story). Note that Robotech and the original Macross and other series are a bit different. We were watching akira by 1989 or 1990.
I distinctly recall that Robotech had a cross-dressing character well ahead of its time (for american audiences).
Well, the point of the _computer_ formalization is that it's checkable.
An error in the formalization would be a bug in lean. Which, as we know, certainly seems plausible (I've mused on if these giant proofs are incentivizing LLMs to find lean bugs to exploit), but at least it's a smaller surface area.
All that needs to be checked to avoid that is the statement of the main theorem. Any divergence further inside means you proved the main theorem differently than you thought you did -- but you still proved it.
This assumes the Lean kernel itself isn't bugged, but getting it correct is a matter that affects all uses, not just this one, so the cost of making it correct is spread over all those uses.
> There is one other aspect of the situation that I would like to emphasise. After two weeks of very
hard work, I have managed to understand only a small fraction of [TC26a]. When I ask Fable about
the paper, it seems to read and understand the whole thing in just a few minutes, even starting
from a fresh context. I know that some readers may be uncomfortable with my anthropomorphic
terminology, but I believe that “understand” is accurate, in the sense that the LLM seems to be able
to correctly and lucidly answer all kinds of questions about the paper, including about some very
fiddly technical details. That is exactly how I would tell that a human colleague has “understood”
something. This chasm between human and LLM “speed of thought” is unsettling to say the least.
This is very odd, because it just doesn't match my experience with these systems at all. Yes, they do generally SOUND confident, but code (say) that's hard for me to understand is usually hard for the machine to understand as well, and while it is more indefatigable than I am, it's not brighter.
This mathematician is in a very good place to evaluate whether Fable gets it or not, but it's weird and counter to my experience.
I would indeed expect most modern models to read the paper and be able to answer questions about them, usually even in a manner consistent with the original intent, irrespective of whether the source material is correct!
Heck, I can do this too, with my eyeballs and brain! Just slower and will less overall memorized knowledge than modern LLMs.
All models still gets things wrong. Even Fable 5.1 I have to regularly correct when working on sufficiently complex code. So, I still want models to get smarter!
Fable is good, especially at conceptual stuff, don’t get me wrong, but it has limits. Opus 5.5 is a machine at getting correct code out once the concepts are in place. But I can’t trust either to not make mistakes.
As an aside, getting things wrong isn’t simply about not being smart enough, it’s also about the model insufficiently assessing whether it actually knows enough to conclude that some hypothesis is correct. As a human I have inner feelings of certainty and uncertainty regarding the things I am thinking about, which guide me in what I need to ascertain or verify more closely. My impression is that LLMs are lacking in that area, and it’s why they are most effective when there are external verification mechanisms.
But your code was probably written by a human. This proof was generated by an LLM. Is it surprising then that it’s easier for an LLM to read than for a human?
Because a math proof is generally de-composable into smaller constituent arguments that can be independently evaluated for correctness. So you can audit a sample of these arguments for correctness without reviewing everything. You would then verify that the arguments being true implies the conclusion.
These models have no self awareness. I just spent days having it write some test framework with very clear goals and it was highly confident understanding exactly what I wanted only for the whole thing to be complete bullshit, one remark from me about the work being useless and it goes “oh you’re absolutely right that’s on me”…
If you read this article, the author is basically saying “the way this worked before was very opaque and probably almost no one figured it out, but _I_ knew how it worked, and so the change is bad for me”.
Do they have a good point that they have a valid use case? Yes. Do they have the only use case? No. Did Apple do this to try to make things better? Yes. That doesn’t make them “evil”, that makes them trying to make things better.
Flat out removing a functionality that is 100% certain to be critical to many without any way of regaining it via any combination of features found on the iPad…
And without any notice whatsoever, and with no way to downgrade back, gets pretty close to flat out evil.
Don’t try to talk out of both sides of your mouth.
Even if they clownishly made it more buried and difficult to find under a dozen submenus… it would still be much less bad in comparison.
(If they never advertised or implied the iPad as being suitable for presentations, education, etc., then that have lessened the severity, but clearly that’s not the case)
it's not hard to accept in general, but have you been following Tao for long? The combination of how virtuous he is with how informed he is with how smart he is is pretty special. He's also far from a luddite. He's been a leader of the computer-math charge.
Questions of AI policy are all hard and anyone who confidently says they know the right thing to do is too confident. Tao's fallible like anyone else, but yeah, as voices to pay attention to go he's very good.
Neil armstrong too should have been listened to .. and just like Tao .. he was quite virtuous, and informed and pretty special .. wont you say so ? and YET he was very vocal about expressing his skepticism about spacex before congress .. thank god his views were rejected .. or we might have missed the magnificent (and now normalised) sight of rockets landing vertically and the incredible engineering behind catching that beast of rocket with chopsticks etc etc
what im suprised about though is why arnt you and others here more suspectful of Tao's skeptisim of AI .. as Wittgenstein's ruler reminds us teh very thing we use to measure something else may itself need measuring .. so why should tao's expertise be any exception?
I'm not saying Tao is right, but (a) he knows a LOT more about about what's actually important in research math than I do (and probably than you do) (b) he's not just having a knee jerk reaction. Tao has been a major leader and advocate for computer-assisted math, including AI, and I don't think that has really changed. He's advocating for how to do it well. He's far from an AI skeptic protecting his turf. Is there any other person as well-versed in research mathematics AND AI-math as Tao? Maybe a few, but not many.
It seems like your inclination is to discount his experience with research mathematics. I agree with you that that's probably what Taleb would do - Taleb has a giant ego and basically operates under the assumption that everyone else has the same giant ego as he does but is (a) less honest about it (b) dumber than he is.
Taleb does have an obnoxious amount of ego, especially in his one on one street fights on Twitter, but his writings have zero ego .. on the contrary, his books force you to take a deeper look at yourself and almost haunt you if you try to BS your way out of confronting what those ideas expose about your own thinking ..
I also read and re read the link you shared .. it’s almost baffling that he is so incredibly hesitant on not being able to clearly take a position on anything and is so painfully nuanced in his writing as if he’s almost hedging every sentence ..
PS: All my life, mathematicians were made to look and portrayed like the ultimate truth seekers (both at school, by the media, in films and in the sciences etc) and all I see is in Tao is a man trying to so badly hold on to the main character energy … perhaps demonstrating a bit of humility like Lee Sedol after loosing to the machine would be in order … in his own words, he sees himself as a fox, not a hedgehog.. guess now that he's been outfoxed .. its best not to say unhinged stuff like "there's no reason to be this fast" or that absolulty out of touch "Math 2.0" cancer slide ... what. an. absolute. tool.
reply