The freedom of speech in the USA is very individualistic, just like everything else. Little to no things are thought of in the sense of a community, it’s all about what’s in it for the individual. Traffic is even more car-centric than in Europe. Pure capitalism without a real safety net, because the individual may benefit from it by becoming a millionaire.

In Europe, the sense for community is much stronger, which is also reflected in how freedom of speech is protected in law; Express your thoughts freely, but do not impair the rights of other citizens.

What? It’s written in Germany’s constitution (The “Grundgesetz”, literally “Basic law”) in article 5 that “Every person shall have the right freely to express and disseminate his opinions in speech, writing and pictures”.

Typical Hänsel and Gretel moment

The codeification of mathematics might make AI-assisted mathematics even better in the future. Proof assistants like Lean or Coq are essentially functional programming languages that allow you to rigorously prove statements via code.

Where a regular AI-generated proof might need a human to verify, an AI-generated proof in Lean would only need a mathematician to verify that the statement to be proved is the correct code-ification of the mathematical problem. This would allow for the “next floor” to be built even quicker, because no human verification is needed anymore. It’s just a question of “Does it compile?”, because the logic is baked into the programming language itself.

But for this to work, many, many theorems and lemmas need to be formalized in Lean. Many mathematicians and computer scientists already volunteer, but the sheer number of theorems is too much. Maybe generative AI will be able to help with that. Maybe it already does, but I’m not in the loop enough.

It’s amazing, it looks like it didn’t rise a single millimeter.

This is what Minecraft in real life must look like