I would expect proofs that exploit kernel bugs to look fishy, so someone reading the proof could catch the smell.
That said, I'm sure there's also room for underhanded Lean programming as well, which would be even more interesting.
3,028 karma · joined December 2, 2015
Email local-part: boexahgahk
Email domain: wilsonb.comThat said, I'm sure there's also room for underhanded Lean programming as well, which would be even more interesting.
Metamath isn't a silver bullet in the design space of formal proof tools, but I personally think it just about nails the metatheory we want. Maybe some explicit facility around definitions would be desireable.
This statement itself predicades on a Platonic realist metaphysics! Indeed, what is the ideal against which things are judge right and wrong? I think the psychological roots of Enlightenment rationality run deep in the West, making it brutally hard to usurp.
That said, I think we can go a long way in this one case by just throwing out the "wrong" judement and laser focusing on the particulars of utility that science provides. One zoomed-out facet sees it as a collaborative effort as squeezing out repeatable processes, a la Popper et al.
Proofs of incompleteness theorems, the halting problem, Rice's theorem etc. all share a diagonalization structure. The keyword here is Lawvere's fixed-point theorem[0], but it's a bit of abstract nonsense, so here's a good accessible video on the topic[1].
I'm not sure the incompleteness theorems themselves are immediately and directly applicable to software development, but I find that having several examples of diagonaization proofs bouncing around in my head makes the Lawvere structure apparent. Since proofs are just programs, the pattern is surprisingly pervasive. Futamura projections are one incarnation, which is essentially how many interpreters end up providing "compilation" of programs into standalone binaries.
[0]:https://en.wikipedia.org/wiki/Lawvere%27s_fixed-point_theore...
We define computable numbers to be Turing machines, lambda reduction processes, or whatever your favorite model of computation happens to be. If you don't like this kind of definition, then we need to talk philosophy of computation.
To decide equality, we let your machines clunk along until they both produce a result, which we then compare (using another machine). Hello Mr. Halting Problem. Specific programs are fine, but comparing against arbitrary classes of program is the bugger. This is why discontinuous functions cannot exist in a hardline computable analysis theory.
People sometimes describe me that way when I start asking unbridled questions. Personally, I find that I can activate this mode when trying to connect answers to some sense of life meaning and the myriad ways that unfolds. Many on the receiving end find the experience frustrating, though.
I think we get used to repeatable patterns more than develop comprehensive understanding. The former feels like accomplishment, while the later feels like perpetual confusion, IME.
They're well-known and have a simpler implementation, and we are familiar with their quirks. There is a giant body of useful knowledge built up around standard real analysis. That doesn't really exist if you insist on using only computable numbers.
The computables are also more fiddly in many ways. Because equality is undecidable, you can't have discontinuous functions, you need to carry around error epsilons all over the place, and we lose useful tools like the Heine-Borel theorem, I think.
Try proving some results in PDE theory, and I think you might change your mind.
In general, I find clarity in thinking of numbers as the system that implements them, rather than as platonic objects with individual reality. What does using Old Boring tech buy you over using Shiny New Thing?
https://www.man7.org/linux/man-pages/man7/gitrevisions.7.htm...
git rebase -i master..HEAD
https://www.man7.org/linux/man-pages/man7/gitrevisions.7.htm...
David Metzler has a series of fun videos called "Ridiculously huge numbers" that goes down the rabbit hole of the fast growing hierarchy.
https://www.youtube.com/playlist?list=PL3A50BB9C34AB36B3
BB(n), Rayo's number and friends can get bigger way faster, but they do this uncomputably fast. Launching yourself into arithmetic hyperspace in a controlled way like with the fast growing hierarchy does a much better job of conveying the sheer vastness of finitude.
OP's article got me thinking about Nim with added mechanics that let you get all the way to Feferman–Schütte, hence the above.
In the hypothetical world where 1 is true, what different evidence do you expect to see than in worlds 2 and 3?
If I were an unscrupulous OAI exec and wanted to opticsmaxx in this way, I wouldn't whip up a single, mild incident. Instead, I might burn gigatokens to 0day a few high-profile suppliers, and then have the model responsibly disclose those breaches. If we're willing to lie collude, and cheat, this story is easy to manufacture with at least as much credibility as the huggingface incident but with the advantage of looking way more impressive and spooking less regulators. And if I really were this evil exec, I would spend more than 30 seconds thinking up an even better strategy here.
If, in contrast, we expect models to eventually breach honest and decent attempts at containment, then I'd exist something sorta like this huggingface story that looks like a combination of impressive and incompetent. I'm not sure whether I'd expect it to come out of a frontier lab or a partner or a consumer, though.
> I'm inclined to believe it was intentional or careless at best since simple network and sandbox controls makes this attack impossible.
Forgive the Saucyness here, but impossible? Really? A security researcher that makes absolutist claims like these looks fatally naïve, IMHO.
/r
The Plan 9 Foundation commissions local artists for it's swag at the annual workshops. I'm guessing this article is tangentially related.
I daily drive 9front, so I might be biased.
The Omnia NG is fanless, meaning quiet and power-efficient. It's also small and relatively stylish. The small hardware LCD is very handy, and everything Just Works. The whole package is just so well put together.
There are even people who have gotten NixOS running on it, apparently.
I've got 10Gbps fiber at home (egregious, I know), and the only OpenWRT router I found that can saturate it is the Turris Omnia NG[0]. The price tag is a notch up from others but it's legitimately one of the best pieces of hardware I've ever owned. A perf3 test against an in-town server was able to pull 800 Megabytes per second; the router is no joke.
If you have a thick line to your ISP, I highly recommend!
I believe the authors are riffing off the wonderful 1970 Counterexamples in Topology[0] book. There's a minor tradition of this among the cognoscenti. The topology book is an absolute gem and very approachable if you have working familiarity with the fundamentals.
[0]:https://en.wikipedia.org/wiki/Counterexamples_in_Topology
I'm truly mystified as to why we're doing this. True, shell programming has footguns, but they're not egregiously numerous compared to the typical suggestioned replacements.
Funnily enough, when the issues with these other languages are brought up—like arbitrary code execution on module import—instead of shallow comments, we often cue an informative and interesting discussion.
Why do we HNers treat the shell language so differently?
One of my working hypotheses is that it's due to shell being both ubiquitous and unfamiliar. Everyone uses it but earnest study is rare. That perhaps make it an easy stress sink for our various sublimated frustrations.
I'm an unabashed (heh) fan of shell programming. It really is a beautiful little language once you learn how to think in terms of data streams, dynamic scope, and DSL design.
Off the cuff, notice that the diagonal has n+1 intersection points, and a path that never passes through the diagonal gives a forest via the isomorphism with ballot sequences [0]. Any sequence that does pass below the diagonal can be "rotated" into one that doesn't, and so there are probably n+1 paths in each "path class" on average.
Conversely, this would suggest that all paths contained in just one upper or lower triangle of the square can be counted by the Catalan numbers. Indeed, a 2x2 square has just 2 such paths and (2n C n)/(n+1) = 6/3 = 2.
[0]:https://blog.wilsonb.com/posts/2026-02-27-easy-random-trees....
Maybe. I think the term is just unfamiliar. The word "vector" is equally unhelpful when you first encounter it, but the concept has enough mindshare that we just acclimate.
Apparently, "vector" in the mathematical sense was coined by Hamilton in the mid 1800s, so around the same time as "torsor". It means something like "courier" which is sensible in Euclidean space but kind of divorced from the algebraic definition. You can still see the "carry along" roots if you squint, but I think the same is mostly true of "torsor", too.
In other words, instead of renaming things, maybe we should just evangelize more? Maybe the quintessential example should be radial directions just to hint at the historical terminology use?
The hypothesis seems to be that the idea of affine spaces came out of that theory, for whatever reason, which was subsequently generalized to principle bundles and finally into what we have now. The point is that, at every step along the way, we want to connect the incrementally new ideas to existing ones, and creating a hard break with new, idiosyncratic terminology is itself obfuscatory.
My beef is more with use of the heavily-overloaded words "regular" and "normal" in math, which just seems like lazy naming:
> In the normal extension K/Q, every normal subgroup of the regular representation acts on a normal scheme that is regular in codimension one, whose normal bundle — orthonormal to the regular surface at each regular value — carries a normal operator whose spectrum follows a normal distribution over a space that is at once regular and normal, all indexed by a regular cardinal.
That's like 8 different meanings of normal and 6 different meanings of regular. lol
Thanks for the writeup!