AxEy

> But a human being using LLMs will be much more creative than just LLMs alone right?

I believe so. But the question I was responding to was whether humans working with Lean would be have been more creative.

The speed matters massively. Also it seems that LLMs are... getting to be quite creative.

The point is that the there has to be an idea to try to check. Lean does not give you that.

> Suppose lean in its current state existed 15 years ago, and suppose the math community eagerly started contributing en masse to a shared repository of code. How much of the breakthroughs and longstanding questions in mathematics that we’ve seen answered this year do you think we would have solved?

(Former grad student in math here who has spent whole weeks formalizing in Lean lemmas that would be considered by professional mathematicians writing a mathematics text / paper as obvious ("without loss of generality we can assume that....", "it should be clear that...")

Probably very few or none.

These systems (mostly) don't help you discover new mathematics. They are a tool for formalization.

It just turns out that combining them with LLMs is the secret sauce. LLMs have quite a bit of creativity but make a lot of mistakes. The Lean typechecker never makes a mistake but has no creativity. Get them to work together in an iterative loop and you get what we have now.

I'm not trying to be snarky here, I'm genuinely considering moving north, and am curious:

> "sidewalks are empty, because if you had any money you would be driving."

Not sure this makes me feel safer. I'm guessing you're not suggesting that everyone has money, so why are the sidewalks empty exactly?

Also would you say that Detroit is "walkable"?

Not sure why you're getting downvoted. I've definitely seen behind-the-front-seats screen ad placement and other weird things in ride shares in the U.S. so this doesn't seem out of the question.

A blind person does not have the necessary input (sight data) to make the necessary computation. A car autopilot would.

So no we do not deem a blind person to be unintelligent due to their lack of being able to drive without sight. But we might judge a sighted person as being not generally intelligent if they could not drive with sight.

> "Use cash, and offline tablet or nothing at all,"

Why would I have to use cash if I gave up my smartphone?

> "In some schools of Buddhism, the tradition was to live with only one bowl and one spoon. The practice was to beg daily... "

Interesting. So the practice of (these schools) of Buddhism requires that there be non-Buddists?

The comment you were responding to said that the free tiers were a boon for the poor and you responded that they (under the fork of interest) "left poor people poorer".

I mean I supposed every transaction leaves someone poorer of something and richer in something else. I'm not sure of the point though.

I concede that if the ad companies are willing to forgo collecting X dollars in exchange for showing you an ad then it must be worth >=X dollars to the ad company for the person to see the ad.

But it remains true that the poor person has no way to convert their attention directly into X dollars, and all that taking away the free tier does is make it so that someone who would have made a trade (of their attention for a service) cannot do so.

This assumes that poor people's attention is liquid and can readily be turned to cash whenever they please.

It doesn't matter how much you think my attention is "really worth". If I want the service now, have no cash, but can pay with my attention, I am strictly more enabled than if the service only accepts cash.

> " in many places around the world we kill people society or state considers assholes, including US."

Not really the same as systematically bringing into existence a species with behaviors you find objectionable, keeping them in your proximity so you can experience said behaviors, and then slaughtering them with the excuse that they are all assholes is it?

> "Then we can discuss where is the cutoff line for enough assholishness to go for a slaughter"

When you say that roosters cross this line do you mean with respect to their behavior towards you? I'm guessing this can't be that bad since you're much more powerful than they?

Or do you mean towards other chickens? If so, and if it's really that bad, then surely the best thing is to just not bring them into existence in the first place (not systematically breeding them with the intent of slaughtering them)?