Viewing profile — thomasahle

Has anyone started proving their sandboxes in Lean (or Coq, etc.)?

> I expect a lot of the social anxiety can be mitigated by arranging things so that students get a chance to know the examiners and build a rapport with them ahead of time. That's …

The talk is wild: https://www.youtube.com/watch?v=87DyyMV0kCY > I want to note that every step in the process we discussed has had a remediation applied. The credentials have been …

Nah, Claude will finish it over night

If it's successful, why do you think we'll even know how it did it?

Here's one way it could happen: Let's say there's some circuit that does problem solving of the kind we call intelligence. We dont know what this circuit looks like, but it exists …

> in a world where a CPU itself may have bugs in the way it executes assembly, that seems a bit silly beyond a certain point CPUs are tested so so much more thoroughly than any sof…

> duping is a great way to show people that even the app layer can be commoditized Everyone is already cloning the app layer. There are 30+ claude-code clone, and codex work alread…

> Whereas in the US you only need to go through fingerprinting only once Once for each arrival.

> as long as China doesn't enter the GPU/RAM race China is obviously in the GPU/RAM race. Heard of Huawei, Moore Threads, Lisuan Tech, CXMT?

Yes, but then it should be easy to check of the result you see match the reasoning you see

TIL: > Many providers build their proxy pools by partnering with device owners who agree to share their bandwidth, while others use embedded SDKs in free apps or VPNs. WTF. That's …

I got into YC, immediately got a 6M offer from Google, sold and won.

Do you have a source for this, or just rumors? The responses I get from pro don't feel like ensembles. They are often very one directional.

I used to part time for the (Danish) mail service. The only sorting that was done automatically was the post codes. That was enough to get the letter to the right post office. The …

> After reading the article, the main "case against geometric algebra" I could find in there was that the author does not like the people using/doing research in geometric algebra …

Why do you need individual data for gerrymandering? Don't you only need area level?

> Ban it from the dataset, add it to the analysis. You can choose your own flavor of noise. Not sure exactly what you're proposing, but if the noise is added independently to diffe…

Deepmind and OpenAI have offices in Europe. But I don't think Anthroipc does?

I recently built a very large test bench for System Verilog. I ran a bunch of different compilers on it, including some open source ones. Some of them failed some tests, and it was…

> The rate of fundamental, broad-based breakthroughs lifting all LLM applications has clearly slowed with many of the most impactful recent discoveries being in scaling, optimizati…

Is my website broken?

I'm trying to recreate all the commercial EDA stack in open source. (RTL simulators, synthesis, formal proof tools, etc.) Building compilers has a _lot_ of parallel tasks agents ca…

He used 600B tokens in 30 days. I use more than 150B/month with just 15 codex accounts. 60 accounts is "just" $12,000/month. So Peter could "save" 100x by using monthly accounts. O…

I'm currently choosing between the right formalization for a big hardware project. I'm considering between SVA, TLA+ and Lean. With the former being more domain specific and the la…