evenhash

Agents don’t have infinite working memory…

LLMs benefit from abstractions for the same reasons that humans do. More information in the same amount of text. Fewer working parts to juggle so fewer ways to make mistakes.

What I’m saying is that you can’t just trust what the AI says because it produces a Lean artifact.

The statement of the theorem has to be correctly translated from English into Lean code.

It’s like translating user requirements into code. The code could run without bugs but not do what the users want.

The only way to know the AI did it correctly is to check. You can’t just take it at face value.

"Lean-verified" is not some magical incantation that makes a supposed proof irrefutable. Even disregarding potential bugs in the kernel as others have said.

Say that AI gives you a Lean proof and says it proves Theorem X. It could just as easily give you the same proof but claim that it proves (not X). How would you know the difference?

Nothing can really be considered proven unless a human expert can read the Lean proof and determine that (X as defined in the Lean proof) corresponds to X. The proof (at least the statement of the theorem) must be intelligible to humans to have value.

It's possible people will just start taking AI at its word. Maybe AI says "Here is a Lean proof of X" and we all just shrug and go "Okay, X is proven." But that's not how it works right now for human mathematicians. Why would we apply that standard for AI?

I think that would only follow if the rest of the world’s purchasing power also grows at the same rate (unlikely), or if you were to cease all international trade (uhh…).

> An AI-generated solution always provides ... proof that there is a solution

This is only true in the most trivial sense. A solution is a solution, sure... but how do you know it's a solution, and not an incoherent jumble of words? A human has to review and vouch for it.

Just because the AI gives you an arxiv-worthy PDF, or a Lean proof which compiles, doesn't mean it proves what the AI says it does. The AI could give you the same PDF/Lean code and says it proves the opposite, how would anyone know the difference?

You can't advance human understanding unless you produce things that humans can understand.

This is already a thing? Just replace “robots” with “machines”.

And yet I see videos all the time of Indians running contraptions straight out of the steam age in their shacks to make plastic straws or sandals. Or just doing it by hand. Better machines to do these tasks already exist, but are obviously too expensive for them to afford. Why would these hypothetical robots be any more affordable or disruptive to Indian workers in particular?

If anything I think American blue collars would be the ones to worry about.

> It’s very easy to send an AI agent on an open-ended bug hunt, and if it wastes a bunch of time and effort and finds nothing, no big deal.

No big deal? It’s not like it’s free… tokens cost money.

Sort of. For me it’s more like seeing out of a third eye (while also seeing out of your real eyes). Like how if you put your finger right in front of your face, you can see two images of it at once. With concentration I can ignore what my real eyes are seeing to prioritize the visualization, but the real eyes are constantly pulling my concentration back.

One thing you notice running NoScript is how prevalent Google is.

Even if a site doesn’t monetize with Google Ads, there’s a decent chance it’s pulling a script from ajax.googleapis.com, and Google still knows that you visited the site from the Referer of the script download.

If what you’re saying is true, what’s the use (or even meaning) of being “all in”? You’re a rock either way.

This is where I’m at as well. If it needs to change too much to do what I want, I take that as a sign to either (1) ask for a change that is easier to review, or barring that (2) pivot to refactoring the codebase until it becomes a change that is easy to review.

Ironically, even in this era of cheap and instant code, what works best (for me) is still to write as little code as possible.

Being “verified in Lean” doesn’t magically solve the problem of hallucinations unfortunately.

It just shifts the work from

> reading the (natural language) proof and confirming it has no errors

to

> reading the Lean code and confirming it correctly encodes the theorem

For example here is a statement of the Pythagorean theorem in Lean:

theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ <-> angle p₁ p₂ p₃ = Real.pi / 2

This is just one possible way of formalizing it and it depends on other definitions, wherein you also need to understand the assumptions they make, etc.

Answering the question of “whether proving this theorem in Lean proves the Pythagorean theorem” thus requires expert judgement as well as domain knowledge of Lean’s libraries.

So if the AI says “this theorem is true, here is the proof in Lean” it’s still possible that it’s not correct, even if the Lean code compiles. The result will still be in question until a human expert reviews it.

I’ve found it depends on where I connect from. If I’m using my home WiFi, it works. If I use 4G or a VPN, I get the login prompt. Still seems to work on my WiFi at the moment.

It’s not crazy when you consider that their customers are the advertisers, not you. They want to keep their customers happy and buying more ads.

Not everyone works for Evil Corp. I work in the public sector and my work supports public health and safety initiatives. AI has allowed my team to get much more done than we would have otherwise which improves the quality of life of the people in my community.

So I would like to counter your cynicism with a “YMMV” depending on who you work for.

> Whilst current models can't 'intuit' and come up with conjectures

People keep saying this. Why?

Surely the AI can complete the prompt “Generate new research questions based on these observations”?

When I read the reasoning traces of coding models they are constantly asking themselves questions and attempting to answer them.

> Nobody is saying we’re going to make the original content inaccessible through the previous means after the LLMs are trained on it.

Is that not why they’re shredding the books when they’re done with them?

In 2026, everything is server side. Serve your DOM updates encoded in JSON if you want. Personally, I find serving them in HTML to be less of a hassle.

> it has clear platform dynamics. It is an aggregator of AI models, and once enterprises use it, that creates switching costs since all your AI expense is in one place: logs, budgets, etc, so switching would be painful and generally not make a lot of sense.

Clearly what we need is a Router Router, to avoid router lock-in.

It would be better to just give the students the money and let them spend it as they need.

If I were a student living on a measly $1600/month I would be livid if the school gave me a $200 raise in AI credits, instead of money to buy groceries or pay rent.

The search space for a naive brute force of three polynomials of degree <= 7 with integer coefficients <= 12 is roughly 10^500. I think it would take a little longer than that.

They do, unquestionably.

https://www.thetimes.com/world/article/google-bans-father-ov...

> Mark, from San Francisco, had noticed swelling in his son’s groin and used his phone to photograph the problem to get an emergency appointment in February last year. He shared the pictures with a nurse so that a doctor could review them.

> However, Google’s artificial intelligence system used to detect child abuse flagged the image to the police and Mark, a software engineer who asked to be identified by only his first name, was investigated and lost access to his Google accounts. He was exonerated by the police in San Francisco but his Google account has not been reinstated.

First party makes no difference, an API can be created for any website or desktop application and served over a network to anyone. It just takes more effort.

Right. Somewhere there’s a dashboard which lists those 6 hours as time saved.

In America?

Probably a better chance the firm privatizes the government.

In fact we seem to be firing government employees and dismantling government institutions as much as possible.

Sure, but wouldn't the leverage of labor go to zero regardless, in this full-automation scenario?

I don’t think people are “underplaying” it, it just doesn’t matter. Engineers aren’t hired for their locomotive skills.

> The issue is that, if we don't do it, China will.

These AI companies aren’t state enterprises. How is geopolitics a justification?

If it were just the military training them, probably no one would care about the copyright infringement angle, it makes sense that the government could ignore those rules for national security.

But Mark Zuckerberg isn’t training his models to protect us from China. He’s doing it to make himself even more ridiculously wealthy.

That ”but what if I win” is realistically what you’re paying for if you buy a ticket.

Maybe the sum of enjoyment lottery participants get from daydreaming about winning is >= the cost of running the lottery?

You have to quote this part to really appreciate how self-contradictory this article is.

> We received almost a million applicants for 1,111 paid internships this summer.

~1000 applicants per internship! Not a job, an internship. How could that be interpreted as anything other than bleak?