Feels like every time formalization is mentioned on hn somebody mentions incompleteness as though mathematicians in the field have never heard of it. It’s kind of annoying at this point. It’s like if every time we talked about a computer algorithm someone popped in to say “Have you heard of ‘On Computable Numbers’? Alan Turing would like a word.”

People in the field know about these things probably better than we do. They are aware of the consequences of completeness/incompleteness, decidability, computability etc. In fact Goedel’s completness and 2 incompleteness theorems have been formalized in lean as part of mathlib4 https://formalizedformallogic.org/Book/first_order/goedel1.h...

Perhaps you'd like to explain how you think the Incompleteness theorems affect this project?

Here's a really good and accessible intro to Langlands https://www.youtube.com/watch?v=4dyytPboqvE

1. Totally ok if it doesn’t look good.

2. Identity is not important. It’s fine if it looks totally generic

3. I don’t care about print/screen/merchandise so it can look terrible in that medium

In general, people want things that look distinctive and work for digital and physical media.

And to answer your question directly, DEC had a whole series of things called "Alpha". eg AlphaStation family of workstations, the Alpha AXP series of processors etc (alpha 21064, alpha 21164, alpha 21264, alpha 21364).

Alpha Centauri (oh no, that's the star system).

Alpha-gal syndrome (oh no, that's the allergy to red meat you can get from being bitten by a tick).

Alpha-bits (oh that's the breakfast cereal)

Alpha course (oh no that's the thing for if you're Anglican and still want to feel like you're in a cult)

Alphabetti Spaghetti (actually I think that was Google Deepmind probably)

....

[1] “Newsnight” on BBC

[2] As in Diffie-Hellman etc https://en.wikipedia.org/wiki/Whitfield_Diffie

   > I can see how it is fraud, but how is it different from all the dark patterns used by newspapers to generate more page prints (like auto-refreshing pages)?

So to answer your question, it’s not a crime to publish an AI-generated song, but it is a crime to commit fraud.

It’s not like it was an actually good coffee machine that has an app to select espresso profiles like a Wendougee Data S or something.

Everyone. I don't think many people working in fluid dynamics were surprised you can find a blow-up in Navier-Stokes. What would advance human knowledge is understanding the situations in which a blow-up might occur. In that context, the lean proof is necessary, but the non-lean proof is more important.