Hacker News: empath75

New comment by empath75 in "I built the RealWorld app in Lean 4"

empath75 — Sat, 17 Oct 2026 14:37:27 +0000

It isn’t but the borrow checker has a formal proof that does need mathlib.

New comment by empath75 in "Desire to Move Permanently to U.S. at New Low"

empath75 — Sat, 17 Oct 2026 12:44:07 +0000

Deporting someone that arrived here 20 years ago, who has a family, whose spouse might be an American citizen, who might have American citizen kids, grandkids, friends, employers, they might own a company and contribute to the economy, etc absolutely is a moral atrocity. Violating border crossing laws is not a crime that is worth upending so many lives. It’s a misdemeanor and the fact that you have to elevate it to a bank robbery to make it seem reasonable tells you everything you need to know. Not all crimes are worth ruining lives over.

I am in favor of deporting people that have not been here long, but there has to be a way to fine people and get them documented after a certain amount of time.

New comment by empath75 in "I built the RealWorld app in Lean 4"

empath75 — Sat, 17 Oct 2026 12:31:44 +0000

I am currently working on a language compiler in lean and it seems to be fine, but compilation times are horrific and having a mathlib dependency just to build a programming language is a big ask for people.

OTOH, my borrow checker is provably sound, which is why I am using it.

New comment by empath75 in "Desire to Move Permanently to U.S. at New Low"

empath75 — Fri, 16 Oct 2026 17:43:15 +0000

[flagged]

New comment by empath75 in "Desire to Move Permanently to U.S. at New Low"

empath75 — Fri, 16 Oct 2026 17:38:45 +0000

Deporting illegal aliens might be popular as an abstract concept but as soon as the question is about deporting actual people that they know, their opinion changes. It’s great politics to say you’re going to do it, but bad politics and a moral atrocity to _actually_ do it.

The only ethical way to do it is better security at the border and making legal immigration and visits much easier. You can’t just snatch people who are established in communities and put them into camps without leading to a thoroughly justified moral outrage.

New comment by empath75 in "Ask HN: Why do people say "I built it" when we should say "Claude built it"?"

empath75 — Wed, 14 Oct 2026 13:18:41 +0000

Why do people say they built it, when LLVM built it. They didn't write any assembly code themselves.

New comment by empath75 in "Scientists wonder: Is my AI stealing my ideas?"

empath75 — Tue, 13 Oct 2026 18:29:12 +0000

If you're working with an AI to solve a mathematical problem, presumably it is contributing ideas. I think the scientists might be confusing the LLM's ideas with their own.

New comment by empath75 in "BB(10) > Graham's Number"

empath75 — Tue, 13 Oct 2026 18:24:10 +0000

I think people are confusing two ideas.

for all n there is some natural number x such that BB(n) = x

x like all natural numbers is trivially computable.

But BB(n) as a function that you could run and _find_ x, is not computable in general, because it would entail solving the halting problem.

New comment by empath75 in "AI models may be capable of self-replicating without access to a datacenter"

empath75 — Tue, 13 Oct 2026 17:22:43 +0000

The nightmare scenario is an AWS or Azure zero-day given to a swarm of openweight agents.

New comment by empath75 in "OpenAI, the Partition Principle, and Mathematics"

empath75 — Fri, 09 Oct 2026 13:35:55 +0000

I think eventually there will be sort of a centralized more or less automated repository for ingesting and sorting ai-generated lean proofs and making them searchable and re-usable. On some level it kind of doesn't matter if mathematicians can ingest the results, if coding agents can just search for them online and use them in their own proofs.

I actually think it would be very smart for the big AI labs to get together to fund an independent organization to manage such a thing, and hire mathematicians to run it.

What is happening now is that some aspects of mathematics are turning into essentially an exercise in software engineering. It is well known that proofs and computer programs have an isomorphism, and I think the eventual merger is more or less inevitable.

That's not to say that there isn't an infinite amount of work remaining for mathematicians to do. There are only so many problems that are going to be amenable to this approach.

New comment by empath75 in "OpenAI withdraws three mathematical results"

empath75 — Thu, 08 Oct 2026 15:27:37 +0000

LLMs find flaws in human-published math papers _all the time_, usually in the process of formalizing them in lean.

New comment by empath75 in "The Mathocalypse"

empath75 — Thu, 08 Oct 2026 13:43:40 +0000

IME as claude works through a problem it develops its own internal vocabulary to describe things, and then the end result is often totally unreadable.

New comment by empath75 in "Navier–Stokes Lost in Translation"

empath75 — Thu, 08 Oct 2026 13:41:33 +0000

If you have ever worked with claude code and lean, it goes back and forth between lean and NL reasoning. I have done a few proofs with claude and it almost _never_ gets the argument right in prose. It usually has to go into lean and grind through proof obligations and then it finds problems, work arounds etc.

New comment by empath75 in "OpenAI Withdraws 3 Math Papers"

empath75 — Thu, 08 Oct 2026 13:39:30 +0000

Because they have hundreds of potential proofs they were sitting on, and lack the internal expertise to judge them. It seems like they're working to formalize all of the in Lean, but that takes time.

New comment by empath75 in "OpenAI Withdraws 3 Math Papers"

empath75 — Thu, 08 Oct 2026 13:37:47 +0000

It is wild to me how much stock mathematicians put into the social aspects of math. The whole social framework you are describing _did not exist_ for almost the entire history of math. It might very well be seen as a historical anomaly, like renaissance mathematicians challenging each other to solve cubic equations.

New comment by empath75 in "Navier–Stokes Lost in Translation"

empath75 — Wed, 07 Oct 2026 19:16:45 +0000

Claude could not fix them without a lot of help, so i did not relinquish sorting through those details in general. Just the drudgery of grinding through proof obligations.

New comment by empath75 in "Navier–Stokes Lost in Translation"

empath75 — Wed, 07 Oct 2026 16:34:59 +0000

> If the lean proof doesn't match the natural language one (which is the one the AI generated to solve the problem), it sounds like the lean proof isn't verifying the intended claim?

No, the other way around. The natural language proof was derived from the lean code, badly. This is my experience with using claude and lean to prove things. Its natural language explanations drift a lot from the lean, both before and after. But the lean code is the lean code.

New comment by empath75 in "Navier–Stokes Lost in Translation"

empath75 — Wed, 07 Oct 2026 16:32:22 +0000

Yes, exactly. There's no real pressure on AI to get the natural language version of the proof correct, and no way to really judge it automatically.

New comment by empath75 in "Navier–Stokes Lost in Translation"

empath75 — Wed, 07 Oct 2026 16:24:42 +0000

I recently spent 3 weeks with claude formalizing a CS paper about a borrow checker in lean, for a personal project.

The formalization went through, but there were _several_ mistakes in the original paper that it uncovered, from type setting errors to (many) formulas that quantified over all resources as printed, but actually applied to only arising resources in the calculus..

So the formalization did give me a formally verified borrow checker that I could use to build a programming language on top of, but it was _not_ exactly the borrow calculus that was printed in the paper.

I expect this is the most common experience when mechanizing a printed paper. There are a lot of skipped steps and handwaving.

New comment by empath75 in "Nearly 200 people under observation after Irkutsk lab worker dies from plague"

empath75 — Tue, 06 Oct 2026 16:17:06 +0000

Russia has bioweapons labs and specifically did research on aerosolized anti-biotic resistant plague.