-
Just ‘42’ tells us nothing.
When producing answers is no longer the distinctive skill of a mathematician, what is the value of an answer? Some thoughts on output versus competence.
-
Auto-formalization II: Now What?
Auto-formalization works. What comes next for Mathlib, costs, definitions, and the human role in mathematics?
-
Auto-formalization I: Keep Trying
I tried auto-formalizing research math in Lean with Claude Code. This first post describes the project; interpretation and outlook will follow in a separate one.
-
Wissenschaftskommunikation im Fediverse
Wissenschaftskommunikation findet heutzutage größtenteils auf geschlossenen kommerziellen Plattformen statt. Intransparente Algorithmen entscheiden dort, welche Inhalte sichtbar werden und welche nicht. Die Universitäten haben sich den kommerziellen Mechanismen weitestgehend unterworfen und versuchen mit allen Mitteln, die Algorithmen zu bespielen. Das Fediverse, ein dezentrales Netzwerk auf Basis offener Standards, gibt Wissenschaftler*innen, Fachgesellschaften wie der DMV und Universitäten die Kontrolle über ihre Kommunikation zurück. Das ist keine neue Erfindung, sondern eine Rückkehr zu den offenen Prinzipien, auf denen das Internet einmal aufgebaut war.
-
Bachelor- und Masterarbeiten
Hinweise für Studierende, die eine Bachelor- oder Masterarbeit bei mir schreiben möchten.