jey
jey on Hacker News
I'm not a Meta fan or anything, but this does seem kind of tricky to deal with. Specifically that pages/topics which get sudden influx of activity at once can look similar to a coordinated spam campaign. Especially if combined with being flagged opponents who don't want to see that content. It seems like it could be hard to tell the two apart, or at least the false positives seem hard to control.
Can anyone with more experience on these kinds of spam/fraud detection systems could chime in?
Julia gets a lot more benefit out of it because it's compiling type-specialized version of the function all the way down to machine code. So for example, a function that's being called with a `Vector{Int64}` ends up dealing with an array of unboxed ints, not going through dynamic dispatch on a generic array for every operation.
Shrug. It's how I do my research now. There were too many mathematical errors when I had agents writing LaTeX directly, even with adversarial reviews, so now I only read stuff that's been formalized, with whatever kinks worked out along the way.
This headline is completely wrong. The proper coding analogy is more like, the natural-language paper was the "design document" before coding it up, then when coding it up as Lean4 proofs, specific details were realized to be slightly off[1] and corrected while writing the implementation in code as machine-checkable proofs. Which I'm sure is an extremely relatable situation for most of us here. But the paper or "design document" wasn't corrected afterwards.
I also think this "paper then code" approach is now obsolete. The modern way, in AI-assisted workflows, is to first iterate on "derivation sketch <-> machine-checkable proof" incrementally building out your result. You can of course leave `sorry` placeholders along the way and fill them in, so it's not like you're restricted to going entirely bottom-up. Finally, once you have a `sorry`-free proof of your top-level statements (theorems) of interest, you can then work on writing up the exposition in LaTeX based on the lean code.
1. See https://arxiv.org/abs/2610.08144 for details, but an example they point out is that a key bound required 5 additional orders of derivatives (and stated in Lean that way), but the paper claimed that the bound held with only four more derivatives.
Yeah, I found that tricky to parse too. But what they mean is that "Triangles in Sparse Lopsided Graphs" is the technique they used to exhibit "Truly Subquadratic 3SUM and Truly Subcubic APSP"
> As a former mathematician, I'm kind of over them using the LLM for math.
As a non-mathematician who sometimes works on mathematical problems, I find this really puzzling. Why aren't mathematicians excited about the frontiers being unlocked by AI? The ability to discover more of the mathematical universe more readily?
Seems wild that they can code and deploy an update of a critical-seeming component in the field like that. I thought such a firmware update would need extensive QA in the lab, along with root causing why this bug slipped through their processes anyway.
But maybe that's the difference between shipping a controller for F1 versus shipping one for an industrial or consumer product? shrug.
At that scale it seems like you could just solve the KKT conditions directly. Exaggerating but only a little
> > which is that over time, as program changes and evolves over years, things tend to drift toward the more general mechanisms that rely on malloc/free on an individual objects, and the program gets slower and slower
I think the idea is that a small program can organize its allocations and data structures to minimize number of calls to malloc, e.g. with preallocated workspace structs, or slab allocation, and similar approaches. But as a program gets bigger, there's a pressure to have looser coupling, to have subsystems with simple convenient APIs which leads to them doing on-demand malloc calls internally, rather than having consumers pre-allocate their needed workspace. Because that kind of workspace management results in more complex APIs and more burden on the consumer.
That said, I don't really believe it either, at least for the kind of codebase where it would matter (scientific computing, in-memory DB server, etc). A codebase that places an emphasis on minimizing heap operations in hot codepaths can do so by consistently using workspaces and allocation-avoiding APIs. I don't think it's so difficult really, but it does take a conscious design decision to do so. But writing something like a web browser in this way could be annoying due to most data having wildly variable sizes, and zig's arena concept would be very handy -- but rust has crates like bumpalo for that purpose.
My personal mantra: "Think in FORTRAN, code in Rust/Julia/C++". But I'm mostly working on HPC-style code where I don't have to do with wildly varying input or output sizes.
> I did not like, and did not understand, epsilons and deltas.
It's nice to have this perspective validated by someone like Serre! I felt like I was missing something when I first encountered that formalism. In fact, all of my introductory calculus classes sucked and turned me off of math for a few years.
Personally I love this concept. I’d be able to stop carrying my laptop around and just monitor/respond to things via SSH from my phone.
You sound like you actually want to just generate them yourself using ArgyllCMS `targen` and `printtarg`.
None of this makes sense or is supported by the facts. Stripe is reportedly valued at $159B, PayPal's market cap is currently $52.59B, and your claims about memes and Wall St are asserted without any citations or facts.
Yeah, that was my reaction too. But there is a subfield called interventional radiology, perhaps GP post is referring to that?
This might just be realistic about the median American's tolerance for walking. Most Americans live in suburbs that are not walkable. At least, I know my own tolerance for walking is very abnormal for an American, and it's due to having lived in walking-oriented cities like Berkeley.
Obviously the costs will come down over time. And quickly.
I'm not a mathematician, but I don't think that's true..? It's just that some problems are considered "hard" or known to have been "open" for a long time or that involve some clever/pioneering new technique. There's tons of math papers out there that are in some technical sense a novel contribution but in practice just languish without much attention except maybe from like two other people working in the same subfield.
> Emojis don't even render the same on every platform
This is a feature, not a bug. That it's using your platform-specific emojis makes it easier to scan, since it's the ideograms you are already accustomed to. Much faster to scan familiar symbols than to read each section heading serially.
I thought other reporting claimed that a ground handling truck crashed into the door, thereby detaching it?
I'm not convinced this is a problem. For example, all the folks who developed convex analysis for its pure geometric and mathematical beauty in the land of pure Platonic forms, well their work was still useful downstream for all of us doing convex optimization and dealing with log-concave probability distributions. So no harm, no foul.
Try the textbook Elements of Information Theory by Cover and Thomas (2006)
It targets x86-64/ELF? I thought it would target `sh` to be portable?
That doesn't really explain anything biologically. Just vaguely says "potentially helps heal and protect"
What does the stem cell treatment help with beyond the existing fetal surgery? Since it's in addition to the usual surgical treatment
And I would further add: In addition to performance, Julia's language and semantics are much more ergonomic and natural for mathematical and algorithmic code. Even linear algebra in Python is syntactically painful. (Yes, they added the "@" operator for matmul, but this is still true).
I wonder if there's a law+econ analysis of comparing the current framework (regulations and upfront permitting) vs having the regulations but then enforcement via combination of randomized gov't inspections and private lawsuits. The motivation would be to allow things to move faster while also requiring the same degree of compliance, but without the massive red tape upfront with administrators having no real incentive to approve projects or move fast. One obvious downside is that it effectively creates an economic incentive to try and skirt the law and/or find loopholes, but that arguably exists to the same degree in the existing system.
