Tootfinder

#Leanstral: #OpenSource foundation for trustworthy #vibecoding
https://

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: @…

Aus dem Tagebuch eines #lean-Learners: Drüben beim @… hatten wir diese Frage: https://podcasts.social/@Eigenraum/116311426809052356
Klar kann man das mit Python einfach durchrechnen, aber ich will ja lean lernen. Also wollte ich das mal formal beweisen.
Wahrscheinlich ein schlechtes Beispiel, weil der Beweis ja tatsächlich komplett rechnerisch ist, aber schauen wir mal: 🧵
@… @…