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.

> The real problem turns out to be the combinatorial explosion inherent in unstructured search through the Herbrand universe. One needs Unification and one needs a still missing ingredient to give search a sense of direction.

Shameless plug: I put together a Jupyter notebook walking through the use of Herbrand Universes for a semi-decision procedure for first order logic: https://github.com/aetilley/harrison-rust/blob/main/Herbrand...

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.

I remember seeing one of these

https://en.wikipedia.org/wiki/Galton_board

at the (I think) Boston Science Museum when I was a kid. They have some pretty cool videos on Youtube if you're curious.

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)?

> "Personally, keeping chickens has almost completely put me off empathy with them. Roosters are assholes. Into the pot with you."

What a relief that we don't generally take this policy toward asshole humans.

At any rate, it's one thing to eat one asshole chicken and another to systematically farm asshole chicken to be killed.

Why did you stop freelancing?

I have twice attempted to make a Grubhub account and twice failed to solve their long battery of puzzles.

Tangentially related: I've always wanted to write a hello the address that they show during the opening credits of MST3K. Has anyone tried?

>There's the folklore about half of all math papers giving the wrong proof for the right conclusion.

Sorry, what? This is an extraordinary claim.

Does this qualify?

https://www.sfchronicle.com/bayarea/article/ucb-police-seek-...

"The five people were part of a group of about 200 protesters, who on Feb. 26 broke down the door of Zellerbach Playhouse and smashed a window to prevent Israeli lawyer Ran Bar-Yoshafat from addressing a group of Jewish students. Danielle Sobkin, co-president of Bears for Israel, one of the campus groups who invited Bar-Yoshafat, said after the protest that members of the mob grabbed a student trying to attend the event, called him a “dirty Jew” and spat on him."

You beat me to it.

> Audition? Sorry, I don't entirely understand what you mean by that in this context.

I think they mean "audiation".

Yes, I'm quite serious.

You give an analogy of software. I suppose I feel that art differs from this in some ways. E.g. originality, creativeness.

Reading many of these responses I'm gathering that perhaps I have too strong a notion of what kind of quality of music might be in demand. While the loops on the original article are impressive given their generative nature, I suppose I felt that there may be a demand for something more (Better sound design, more long term structure), but maybe I'm naive.

But thanks for giving me your perspective.

Honestly what I'm most excited about is how this technology can be used, not to arrange parts or even loops but rather in new plugins (VSTs) that implement novel approaches to digital synthesis. Think of all the awesome sounds.

If anyone knows anyone working on that, ping me. :)

It was not super discerning listeners (like it sounds like you are) that I meant to address in that second question. Sorry if that was not clear. Rather it had sounded from some of the comments that people were desperate for original tunes (and maybe not necessarily the most highly produced). But I didn't point to a specific comment, so maybe that's my fault.

We may also disagree on how much good stuff there is coming out, but I agree there is a lot of noise.

I get that. It was not those purposes that I wanted to question, but rather just the one near the top of my question, namely demand.

>the simple answer is that your motivations for being an artist need to change to be exclusively personal fulfillment.

Mine are and the same goes for most of the artist I indicate. The point wasn't that they were in it for the money, although many dream of being able to at least one day pay the rent with it (or maybe just groceries).

The rest of your response makes sense (although I think much of it could be said for all of hiring someone to do work). Anyway, thank you for providing your perspective.

(This is not meant to be an anti-ai-generated-art rant. It's coming whether we like it or not. But some of the motives in this thread confuse me.)

Music producer here with an honest question to those saying "this will provide me with a simple soundtrack/background music for $PROJECT"

Have any of you checked out / made offers on music production subreddits? Or other music subreddits? various music production discords? Elsewhere on the internet?

If so, could you say what your experience has been?

I ask because the music production scene is like...ridiculously saturated, and it's almost a meme in the producer community how hard it is to make even a buck producing. I suspect that there are a significant number of producers who would be happy to take your "prompt" for a small fee. Yes, I understand 1) free and 2) immediate is convenient, but isn't 1) relatively inexpensive and 2) whatever advantage intent in construction gives good too?

I'm willing to admit that I'm missing something here, but I'd love it if someone could enlighten me.

While I'm asking follow ups, to all the folks who love digging for new music so much that they're considering turning to prompting AIs, I'd be seriously surprised if you've really checked out all the stuff that is coming out from new producers (again, reddit, soundcloud, etc). Another meme in the producer community is how one spends hundreds/thousands of hours perfecting ones craft, and dozens of hours working on a track, only for that track to get like 5 plays on soundcloud and negligible engagement elsewhere. Are music consumers really that desperate for new tunes? Frankly a lot of us just aren't seeing it....

Perhaps these are all probes dropped off during ʻOumuamua's fly-by?

(mostly kidding...)

I'll be happy to circle back to more modern methods once the core parts of the field are addressed. The point of the library is not really to deliver a competitive solver (yet).

Thanks