seanhunter

The Langlands program is about correspondences between analytic number theory and harmonic analysis. You could think about it as a unification of parts of mathematics that seem to have no reason to join up but turn out to have deep and non-obvious connections. It doesn't have anything to do with formalization.

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

All of them? I mean literally any global brand.

Maybe they will recursively self-improve to the point where they are genuinely competitive with Anthropic and OpenAI, or where they “AI summaries” they add to search results aren’t total garbage most of the time.

That seems pretty standard to me. Consider the counterfactual: How many design briefs do you think contain one or more of the following:

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.

Or the new variant which really turns my stomach “| Life Coach | LinkedIn Influencer”. Just, no.

OK I'm telling you that I'm not as keen as you are to cede every possible name that starts with "Alpha" to Google.

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

AlphaStation (oh no, that was DEC).

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)

....

I remember seeing a TV program[1] where the UK govt had proposed some hare-brained key escrow thing (this is circa 2000 ish) and they had an expert on to discuss it. Well they didn’t mess around. The expert they had on to explain the drawbacks of the scheme was Whitfield Diffie[2] and he was up against some government contractor slug in a suit. Anyhow Diffie explained that there is essentially no security measure that is effective if you create a prize of infinite value. If the prize for circumventing security is great enough, it will be possible to use money to get around whatever security.

[1] “Newsnight” on BBC

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

Gauss agrees with you. He said "If the numbers we call +1, -1, and √-1 had been called direct, inverse and lateral units, instead of positive, negative, and imaginary (or impossible) units, such an obscurity would have been out of the question."

Firstly thanks for writing it and making it available. The problem I had when I tried it is it would consistently blow out the small context window of my local qwen and although there was seemingly a config knob I could use to prevent that, seemingly that didn’t do anything.

Just spin the golden-egg production part out of the goose, then we can cook and eat the rest.

“Now trades well above the IPO valuation” does not mean something would have been a good investment at the IPO price given opportunity cost and the time value of money. Additionally, the current price could equally not represent good value.

Remember he was producing the anti derivative/integral and already had the original expression. So all he needed to do is show that when you differentiate the integral answer you get the original question. That’s a lot easier than you’re making out.

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

Whether or not something else that someone else does is fraud isn’t relevant. You got to the part where you can see that what he did was fraud. That’s why he got a prison sentence.

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

Also, can we talk about the fact that it is a Keurig and therefore makes disgusting swill rather than coffee.

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.

That is frankly, obvious horseshit. It couldn’t possibly be a gamble because you can just trivially differentiate the answer and see if it came out to be the expression in the question.

Yes it is. The existence of a wikipedia page for such a minor piece of internet trolling seems bizarre.

> Who cares?

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.

How this works in the UK normally is when you're knee deep in the purchase process you have to get legal searches and a survey and the lawyers or surveyor will find the tunnels have no permissions and then you will not be able to borrow money to buy the property because no bank will lend when there is an adverse survey or there are legal questions associated.

You can get these types of things sorted (eg apply for retroactive planning permission) and the council will send a surveyor and give you an opinion but you are running the risk that they insist you either make it good (remedy anything they don't think was done right) or (worst case scenario) tell you to put it back like it was before the unpermitted work was done. This happens more often than people think.

That's why the house has been reduced in price so much - to find someone who feels like the headache is worth it. I have my doubts to be honest.

Ziggurat is badass. It’s also one of those algorithms (like “Metropolis-Hastings”) that has a fantastic name to go along with cool mathematical and practical properties.

https://heliosphan.org/zigguratalgorithm/zigguratalgorithm.h...

The reaction of the tech community to this story is extremely strange. If you type some sort of serious credible threat into a Saas platform, or post it on a message board or upload it as user generated content into any tech platform that is hosted in a “normal” country (by which I mean US, EU, Australia, UK, New Zealand, Canada and many other jurisdictions), your threat will very likely be reported to the police.

This isn’t a new phenomenon and it certainly isn’t an AI thing, it is a long-term policy posture that we as a society hold tech platforms accountable for serious threats that they are able to help to prevent that is implemented in a swathe of different legislation around the world, but it’s everywhere. This is clearly a privacy vs safety tradeoff and you can have all sorts of opinions about that, but this has been the case for a very long time (certainly since 2001).

Now different tech giants have different levels of competence at policing content on their own platforms but they all do it. As I say this is absolutely not anything to do with AI except to the extent that the AI companies are probably paying more attention to what is typed into their platform because they are using it to develop their models and the whole “AI safety” debate is evolving rapidly. But that’s merely a difference of degree.

I’ve had “please enter a valid email address “ even though my email address is valid and ends in .com. Some people have terrible validation.

I use lean a lot, reasonably effectively (although I’m still just getting started) but I’m using it as a proof assistant for mathematics. The background that is actually useful for understanding how lean works and most “mathematical” lean use cases is dependent type theory and homotopy type theory. So people who really want to go deep on lean often recommend the HoTT book (https://homotopytypetheory.org/book/) but that’s not required reading for getting started in lean, more like if you’re doing a PhD in formalization or whatever.

It sounds like for your use case of software verification mathematical logic is important, but that’s definitely not the case for most lean users. I wouldn’t say it’s required or even useful if you want to use lean for proving things in general.

This looks really cool. You can see the potential when you consider how automation works in games like “Stationeers” (which allows the player to automate stuff using a mips-like assembly language called “IC10”). A huge limitation in stationeers is the cap on the length of IC10 scripts you can write, so having such a flexible automation platform baked into the game is really awesome.

Best of luck with the game! I am watching with interest and will for sure get it when it hits early access.

That makes sense. You need no background in logic whatsoever to learn lean. For some reason that person was gate-keeping.

I have absolutely no idea why you’re trying to make out that compactness for example is part of the theoretical foundations of Lean, but it definitely isn’t, and it’s so far off-base that I’m wondering why you’re saying things like this.

Compactness[1] is a useful property of some sets. It’s an example of the type of thing you might want to prove or disprove (eg that a certain set in a given metric space is or isn’t compact, or prove the Heine-Borel theorem or whatever), but if you’re not trying to do that, you can go about your merry way and learn a ton of lean without being aware that the concept of compactness even exists.

The same is true of incompleteness for example, which has literally never entered into the realm of being relevant for anything I’ve done in lean, and is definitely not in any way important prerequisite knowledge.

[1] And yes, I really do know what compactness is and I learned that the hard way by working on a bunch of proofs in analysis. There’s really no substitute for learning by doing. A set S is compact if and only if any open cover (ie family of open sets {T_i}_{i in I} such that the union U_{i in I} T_i is a superset of S for some possibly infinite indexing set I) contains a _finite_ subcover (a family {T_j}_{j in J} where J is a finite subset of I and the union over J of all the T_j’s also covers S). Compactness in logic is a consequence of compactness in the set-theoretic sense and really has no relevance whatsoever to lean.

This is absolutely not a helpful list for someone who wants to prove things in lean, and just seems like weird gate-keeping. In particular, Proof Trees are completely irrelevant, incompleteness and compactness are only relevant if you are proving things in those specific fields and the only thing you need to know about constructive vs intuitionistic vs classical logic in lean is if you want to use the law of the excluded middle or some non-constructive proofs and tactics, lean won’t force that on you, so you sometimes need to “open classical”. (And this is covered in “Mathematics in Lean” and “Theorem Proving in Lean” at the appropriate place).

Knowing that the Curry-Howard correspondence exists is important if you care about the CS magic that makes lean work and to understand how term mode and tactic mode relate to each other but again it’s really not necessary to understand the correspondence itself to use lean as a proof assistant. (And this is covered extensively in “Theorem proving in Lean” if that’s your jam).

Whatever mathematical background you have is obviously helpful and will widen the scope of what you can do, but you don’t need to learn a huge amount of foundational mathematics to get your hands dirty in lean. For example, “The Mechanics of Proof” by Heather Macbeth was written as a course for 1st year undergrads so only assumes high school maths knowledge. Here’s a list of learning resources that the lean prover community recommends https://leanprover-community.github.io/learn.html

One thing I would add is if you want to learn about proof writing in general there are a lot of good resources out there including “The Book of Proof” which is free online. https://rcsnyder.github.io/open-frontier-curriculum/07-resou...

I personally really enjoyed Jay Cummings’ “Proof: A long-form mathematics textbook” which is on that list as it provides lovely little intros to various areas of mathematics along the way. I have done every exercise in that book and had a lot of fun in the process.

But these aren’t things you necessarily need to do before getting started in lean.

My memory is ancient so may be flawed but that is what I remember. This seems to be a full chronology of the incident if you’re interested https://www.computerweekly.com/news/1280096804/Chronology-Th...

Computer Weekly in the UK did some pioneering journalism into a helicopter crash[1] that had initially been blamed on the two pilots but seems very likely to have been caused by a failure of a computer system that was controlling the fuelling of the engines. Iirc this system seems to have crashed causing engine failure of both engines in heavy fog, bringing the helicopter down with a loss of everyone on board, however for reasons somewhat unclear, the MOD wanted to cover the failure up by blaming the pilots.

Now this was a windows system[2] rather than linux but the point remains - if there was an external vulnerability in a crucial control system and this system was part of a network (eg to connect telemetry) then any exploit of that system could result in loss of life.

[1] https://www.computerweekly.com/news/1280091718/Chinook-compu...

  After an assessment of the Fadec software the Superintendent of Engineering Systems said that the density of deficiencies was so high that the software was unintelligible.

[2] Which, why? Why build the fuel controller for a helicopter engine on windows?

That is not true. The specific powers of arrest and detention by UK border force were set out in this freedom of information response here https://www.whatdotheyknow.com/request/uk_border_force_power...

Summary is they can’t detain people for no reason, they can detain people for specific offences relating to immigration and citizenship, customs and excise and also the normal stuff any regular police officer can arrest people for.

I’m no apologist for how much state authority they have, but it’s not as bad as you’re making out.