Tootfinder

Me: Using a proof assistant like #lean, we can express all math in an expressive and algorithmically checkable way!
The proof assistant: Consider this simple equation among 3x3 determinants:

BTW, this is 21/21 now:
#lean

Here is a quine in #lean
def main : IO Unit := do
let s := "\n IO.print (\"def main : IO Unit := do\\n let s := \" s.quote s)\n"
IO.print ("def main : IO Unit := do\n let s := " s.quote s)
S is code to print the preamble P, then S quoted and then S.
If you want to test it, make sure there is a newline at the end of the file because S ends in "\n".
#Python:
s = '\nprint("s = " repr(s) s)'
print("s = " repr(s) s)
2/2

Saying something without saying anything in #lean:
def non_decreasing (f : ℝ − ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ − f x₁ ≤ f x₂
example (f g : ℝ − ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : non_decreasing (g ∘ f) := fun _ _ h => hg _ _ (hf _ _ h)
Is this a good proof? It's certainly easy to see after seeing it !!

I just learned an interesting cultural tidbit yesterday: In the #lean community they use the octopus emoji 🐙 to celebrate.
This is because if you use the right font, it looks like the Octopus has two arms raised like his team has just won a cup or something.
It's also featured in this recent Quanta-Article:
https://www.quantamagazine.org/in-math-rigor-is-vital-but-are-digitized-proofs-taking-it-too-far-20260325/
(which constructs some careful criticism of mathlib btw.)
cc: @…

Wanted to report on my (concluded!) auto-formalization #lean project.
The blog post got a bit lengthy and it is only part 1: "What actually happened?"
It took about 2 months to go from zero to a full lean formalization of a paper of mine. I only steered the LLMs and checked the interface to human mathematics (statements and definitions).
I am positively surprised and I do think this will change (my) research math. Ask me anything about it!
#llm #claude

How it's going #leanstral #lean #mistral
Look how it is offering to prove Fermat's last theorem!

Habe heute entdeckt, dass in der Fakultät ein bisher ungenutzter Server mit 2x NVIDIA V100 32GB stand. Und nach einem Treiberupdate lief darauf auch das #leanstral Modell mit vernünftiger Geschwindigkeit.
Habe jetzt die 4-Bit Quantisierung genommen und dann passt es mehr oder weniger in den VRAM. Die Kiste hat 1TB normalen RAM, also kein Problem hier.
Bin gespannt, was das kann!
#lean #mistral