vatsachak

You can embed TLA+ into Lean. I don't think that there's any benefit to formalization before coding unless you're working on like million dollar projects

I don't really buy this argument because we can all read the code with the Lean LSP.

Also, after using a tactic enough you can guess why it's used.

Agda and Idris are more beautiful for sure, but a proof is a proof (according to the law of the excluded middle)

Terrence Tao's blog is better than most textbooks and everyone has been using it for the past 20 ish years lol

Yeah more or less. I proved a SOTA result using Gemini 3.1 Pro a year ago and it was a lot of back and forth.

We're definitely still in the computer chess phase.

And yet it can't even replace a call center employee.

I guess you can't make a career out of being a frog anymore in math.

Yeah. But we need throw money at studying the brain, instead of another billion to "agents which understand you truly"

Super big fan of your work on cellular automata. Do you have anything interesting papers coming up?

Interesting. But, evolution is way too unconstrained to provide us a path to "agi". It would require too much compute.

Evolution also eventually gets frustrated and creates the brain, capable of in context learning.

Maybe we should take some notes from these massively parallel, shallow, and highly recurrent constructions.

Maybe a subset of mathematicians, but if someone proved that RH was undecidable we would still give them the millennium prize.

Very fair. But when you say "What mathematicians care about", you are taking about mathematicians today, who really care mostly about politics

I think that your take is quite optimistic. Having published in top tier journals my only experience is that mathematicians care about what other mathematicians worked on and failed to solve. Theory building papers are dime a dozen and don't get published in high tier journals unless they solve a problem.

Math is such that most theories are built after solving a problem and actually don't solve a larger class of problems. Etale Cohomology is an example of a rare exception. Grothendieck was mad that Deligne used adhoc complex analysis techniques to prove Weil. But everyone else was thrilled.

Whereas in CS, a good theory (library) solves a large class of problems. The reason being is that CS tackles general problems while math specific ones. Math on average solves problems that don't lead to solutions to other problems.

To me at least, math is more of a game like chess and coding is more of an art. There are aspects which are a game, like performance engineering but I'm pretty sure that LLMs will become superhuman at that soon

It's not a problem of incentives. Every executive wants to inject LLMs everywhere these days. If they haven't somewhere it means that it does not work.

Not always, sure but 90% of the time yes.

For example, create a DFA for a regex, not too bad just use Thompson's algorithm and then NFA->DFA. But now we have to care about efficiency, user API, maintainability of definitions etc.

Coding is more of a human problem than math

No it can't. Show me a business which uses in context learning to manage a McDonald's

Math is way more automatable than programming.

In math, a proof is a proof. We don't know if we can get there and so getting there is the hard part.

In software, we always know that we can solve the problem. So HOW to solve the problem is the hard part. Because the type of solution involves maintainability, which involves planning, LLMs suck at it. This leads to "LLM slop code" whereby the LLM creates ad-hoc convoluted logic with redundancies and no reuse of existing standard library batteries.

Unless you're a Grothendieck who gets mad at Deligne for not solving the Weil's conjecture "THE RIGHT WAY", software is fundamentally different than math in this respect.

So I'll say it again, AI will win a fields medal for before managing a McDonald's simply because there are enough big problems within arms reach than their current capacity to plan over time

Yeah pglite is exquisite. Now I don't have to write separate code for client and server side queries.

For example, I have a compiler that compiles a DSL to a DB query which returns a list. Now that query can either be on data in the browser or can be on data on the server. Now I don't have to write the logic twice!

Literally just keymaps

Here's my two cents as a mere paper reader;

JEPA is really just a generalized encoder, so the JEPA created latents should be fed into a transformer trained with either user data or RL policy.

Although the above might not work great either because you said that vertical position was not predicted well!

Great article and I hope that you can carry on with the JEPA research

Automated coffee vending machines are not at the level of barista.

Plus a coffee shop is about the experience, not the price.

But most jobs that aren't service are not about the experience.

The world has been getting richer as everything has gotten automated

RSI isn't anything new though; computers have been used to make computers better for about 80 years now.

Imagine having a secretary who could read 1 million records and give you back your answer in 100 microseconds, for just 10 cents an hour. That's Postgres.

So I'd imagine that if R&D can be automated, everything becomes better and cheaper but we'd all lose our jobs, as secretaries did to postgres. UBI season

Now that's what we call bait

I don't hate SF it's just overpriced.

Whenever I visit SFO it's really funny seeing all the advertisements from startups above a population struggling to find housing.

Won't it be better to pay someone 100k in Reno than 180k in SF? Most collaboration happens online these days anyways.

Honestly 60k in Barcelona is like 200k in SF when you look at housing and public services.

We need to punish bad city governance for being bad.

Creativity can be automated. Humans are automated creativity invented by evolution

I find that Amazon is still the best for new, niche items like stationery. Maybe I need a Bayesian update

Yeah. Target has been more than pleasant, but I know that they have always been good at design and ergonomics.

I should probably just switch to them

Using LLMs to generate dashboards is probably their most productive use case

I use Amazon for niche products. Unfortunately the US doesn't have many niche stores like Japan does

They have a basis in the formal scale. The cool thing about formal logic is that it's all about physical changes.

Now, the meaning of the statements is definitely human, but the proofs go beyond

You clearly have not seen the King of the Hill episode where Hank tries to tackle his anger