Tootfinder

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

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

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

BTW, this is 21/21 now:
#lean

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: