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.
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.
I have long been skeptical of the educational value of non-fiction books. Mostly when I have bought a book on a topic I found interesting, I either never started reading it, abandoned it after two chapters, or skimmed through the table of contents to find just the things that seemed interesting and ignored everything else. When I did read several chapters in order, I mostly did not remember much later.
There are exceptions, of course. Effective Java is one, which is because it is a compilation of many small independent pieces of wisdom each of which is presented in a compact form. Modern Principles of Economics is another, and that is because it is a proper course textbook for a formal curriculum, with exercises and all.
The classic essay-as-book type of book, however, is mostly worthless to me.
Arnold Kling agrees.