What occurs when this process is reversed - translate from lean to informal english, and does iterating this then help research better approaches toward writing proofs in human language?
I had the same thought but unfortunately even if that translation is accurate it could still be bidirectional hallucinating and would not really be sufficient evidence...
It's another reformulation rather than a true proof. Now, instead of wanting a proof of a theorem, now we just need to prove that this proof is actually proving the theorem. The proof itself being so incomprehensible that it can't on its own be trusted, but if it can be shown that it can be trusted then the theorem must be true.
FTA: "While we can’t say with certainty what caused this route leak, our data suggests that its likely cause was more mundane. That’s in part because BGP route leaks happen all of the time, and they have always been part of the Internet — most often for reasons that aren’t malicious."
It's an engineering reason really, the entire reason why MFTs were so popular when they came out was because people were tired of lugging around their Full-Frame camera's zoom lens, and were sick of missing moments when using a prime lens.
The marketing gimmick for awhile was ultra-zooms which allow for smaller lenses via fixing distortion using DSP, but this degrades the image quality, and so never became a solution for RAW shooters.
It's interesting that the Roland DSP does eloquently map to solutions in the z-domain, and allow easy implementation of FIR/IIR filters.
It's not surprising they doubled the clock rate to 88.2kHz to simplify anti-aliasing, but it is curious the choice of the CD audio frequency of 44.1kHz and not the DAT tape frequency of 48kHz.
It's hard not to get nostalgic about the 90s when watching this video.
I mean in a normal math curriculum you would define only the multiplicative inverse and then there is a separate way to define fraction, if you start out with certain rings. It is kind of surprising to me that they did a lazy definition of division.
Just as we had the golden era of the internet in the late 90s, when the WWW was an eden of certificate-less homepages with spinning skulls on geocities without ad tracking, we are now in the golden era of agentic coding where massive companies make eye watering losses so we can use models without any concerns.
But this won't last and Local Llamas will become a compelling idea to use, particularly when there will be a big second hand market of GPUs from liquidated companies.
Yes. This heavily subsidized LLM inference usage will not last forever.
We have already seen cost cutting for some models. A model starts strong, but over time the parent company switches to heavily quantized versions to save on compute costs.
Companies are bleeding money, and eventually this will need to adjust, even for a behemoth like Google.
What I find strange about Google, is that there's a lot of illegal advertising on Google maps - things like accomodation and liquor sellers that don't have permits.
However, if they do it for the statutory term, they can then successfully apply for existing-use rights.
Yet I've seen expert witnesses bring up Google pins on Maps during tribunal over planning permits and the tribunal sort of acts as if it's all legit.
I've even seen the tribunals report publish screenshots from Google maps as part of their judgement.
I was a victim of this when I moved into my house. Being unfamiliar with the area, I googled for a locksmith near me. It returned a result in a shopping center just about a mile away from me. I'd driven past that center before, it seemed entirely plausible that there was a locksmith in there.
I called the locksmith and they came, but in an unmarked van, spent over an hour to change 2 locks, damaged both locks, and then tried to charge me like $600 because the locks were high security. It's actually a deal for me, y'know, these locks go for much more usually. I just paid them and immediately contacted my credit card company to dispute the charge.
I called their office to complain and the lady answering the phone hung up on me multiple times. I drove to where the office was supposed to be, and there was no such office. I reported this to google maps and it did get removed very quickly, but this seems like something that should be checked or at least tied back to an actual person in some way for accountability.
Then I went to the hardware store and re-changed all the locks myself.
It definitely sounds like a hard problem. I'm not familiar with the current process, but based on what I found when I looked it up, it seems like there is a verification step already in place, but some of the methods of verification are tenuous. The method that seems the most secure to me is delivering a pin to the physical location that's being registered, but I feel like everything is exploitable.
Why does Google get to say 'its hard' and we have to give them a pass? If a business is providing a service, they need to ensure it is doing what it claims. Whether it is difficult or not is not our problem.
Locksmiths and plumbers is especially one of those things that they've figured out how to game the system to get an extra expensive service that they contract with instead of a local company that is less expensive and doesn't have the middleman.
Reminds me of Trap streets or Trap towns that cartographers would use to watermark their maps and prove plagiarism. The trouble is reality would sometimes change to match the map.
Is it treated differently from other kinds of advertising? A lot of planning and permitting has a bit of a 'if it's known about and no-one's been complaining it's OK' kind of principle to it.
reply