Documentation for Mathlib for Lean 4.
The Lean community maintains Mathlib, among other things.
The official Lean 4 manual.
A book on modeling mathematical objects in Lean 4 and proving their properties.
A book on Lean 4 as a theorem prover (as opposed to a programming language).
A book on Lean 4 as a programming language (rather than as a theorem prover).
Das fällt einem Netzbetreiber jetzt plötzlich auf, nachdem das Bundesverfassungsgericht die Schuldenbremse scharfgestellt hat.
Warum nicht gleich so? Weil „Proteste und Klagen von Anwohnern und Landschaftsschützern“ wichtiger waren als Kosten. Klar, wenn so ein wohlhabender Vorstadthausbesitzer herumjammert, dann ist es es natürlich wert, dass dafür jeder von uns (Kinder und Rentner eingeschlossen) € 200 zahlt. Hauptsache, die Sicht auf die Berge und den See ist nicht behindert.
Wenn ich der Staat wäre, ich würde mich nicht von so einem Gequengel 20 Mrd. Euro in die Höhe treiben lassen, sondern ein Gesetz erlassen, das Anwohnern und Landschaftsschützern die Klagebefugnis nimmt. Dafür würde ich ihnen großzügig das Recht einräumen, den Aufpreis für unterirdische Leitungen in ihrer Gegend selbst zu zahlen. Dann würde sich schnell zeigen, wieviel es ihnen wirklich wert ist.
Stable Rust ABIs via Rust-to-Rust FFI.
C, C++, Rust, and CUDA build cache. Also supports distributed builds and the GitHub Actions cache.
A version number management tool based on conventional commits with support for monorepos.
Basically:
- Do not take your kids by car (it’s just bad in every way)
- Send your kids off alone once they are old enough (my personal rule of thumb is 2nd grade, but of course every child is different)
Enter your income and assets and find out which class you are in (if you live in Germany).
A cheatsheet.
Framework for testing operating systems against both real and virtualized hardware. Used by KernelCI, among other things.
Backend for xrdp.
X11 RDP server. Supports drive mounts and audio redirection.
A book by Tyler Cowen, but not just a book. It comes with an AI companion that you can ask questions about its content. To me this seems like such a clear improvement over a simple book that it ought to become the default for nonfiction literature.
Matthew Yglesias makes the point that the United States would be wise to grow in population so it stays relevant and strong.
Matthias
#
Dealing with the population crisis
Here is a set of political positions that, even though they go together naturally, in combination will offend everyone, both left and right:
- Most of the developed world aligned with the West, including Western Europe and the United States, suffers from a fertility crisis. This is bad. We need more people if we want to (1) stay at the top of the world order rather than drop to the bottom and be dominated by bigger players and (2) keep our national economies going and continue to produce more prosperity.
- Therefore, we need more immigration. This is emphatically not limited to highly skilled workers, but includes low-skill, less productive immigration, too. After all, we need both more production capacity and a bigger market, and each additional person helps with both (unless they are very old or sick, but those tend not to be the people who like to migrate anyway).
- At the same time we have to reward people for producing more offspring. This very likely means that significantly more resources need to be diverted from singles and single-child families to families with 2 or more children, so much so that not starting a family early on is taxed substantially. This will be a regression in both personal freedom and gender equality, but lead to a much-needed recovery of fertility.
People as different as Robin Hanson and Matthew Yglesias have written about the topic – not necessarily in the way I summarized it above – but I have yet to see a party platform that incorporates all of it in combination.
FROM ghcr.io/macoscontainers/macos-jail/ventura in container files? Intriguing.
It uses rund under the hood, which means it is not very isolated at all. Still, I am sure there are use cases.
A game library manager for GNU/Linux. Installes games from Steam, GOG, and Humble Bundle and manages the compatibility runtimes Wine, Proton, DOSBox, ScummVM, and RetroArch.
Key points:
- The Democrats talk about climate change and student loans a lot. They do not talk about healthcare as much.
- The public is significantly more aligned with the Democrats on healthcare than it is on climate change and student loans.
- This is dumb.
I suspect analogous points can be made for liberals and progressives around the world.
Here in Germany, for instance, the left and center-left parties like to talk about feminism, gendered speech, trans rights, and refugees’ rights, all things that while morally commendable, they do not have a popular position on. The politicians that tend to get the votes are the ones that take more moderate or even conservative stances on these questions.
Climate change, meanwhile, is a topic that the center-left has popular support on around here. Even there progressive politicians and pundits often focus on the negatively connoted things, such as bans of environmentally harmful practices and industries. Instead they should communicate their successes more forcefully and focus on an abundance message based on cheap wind and solar energy.