Andreas Becker14h ago

Mistral AI präsentiert das Modell Leanstral, das Quellcode durch Lean 4 mathematisch verifiziert.

Das System nutzt eine Sparse-Architektur mit 119 Milliarden Parametern, wovon 6 Milliarden pro Aufgabe aktiv sind. Im FLTEval-Benchmark erreicht es bei vier Durchläufen 29,3 Punkte und steht unter Apache-2.0-Lizenz bereit.

#Leanstral #MistralAI #Lean4 #OpenSource #News
https://www.all-ai.de/news/news26top/mistral-leanstral-neu

Diese neue KI prüft ihren Code mathematisch auf Fehler

Mistral bringt ein Modell auf den Markt, das Software mathematisch auf Richtigkeit prüft. Die Benchmarks überzeugen.

All-AI.de
N-gated Hacker NewsFeb 21
Lean 4 is apparently the new secret sauce of #AI dominance, because who knew that theorem proving could be so *riveting*? 🤔✨ But don't worry, before you can learn how to take over the world with math, you'll need to pass the Vercel Security Checkpoint IQ test, where only the chosen ones with #JavaScript enabled may proceed. 🛂🔒
https://venturebeat.com/ai/lean4-how-the-theorem-prover-works-and-why-its-the-new-competitive-edge-in #Lean4 #TheoremProving #VercelSecurity #HackerNews #ngated
Hacker NewsFeb 21

Lean 4: How the theorem prover works and why it's the new competitive edge in AI

https://venturebeat.com/ai/lean4-how-the-theorem-prover-works-and-why-its-the-new-competitive-edge-in

#HackerNews #Lean4 #AI #TheoremProver #CompetitiveEdge #MachineLearning

Show threadAndreas GroisFeb 18

This is also not too different to how #Lean4 implements mutability and loops in its do-notation.

(Though I think Lean does not use a key-value-store, but rather just nests multiple State Monad Transformers inside of each other.)

shnarazk   🎄Feb 6
  • public import LeanDag DONE!
  • let is ignored 😲
  • long lines are trimmed 😠

#lean4

Lukas GerlachFeb 5

A sizable refactoring (basically almost a complete rewrite) of the Chase definitions in my #Lean4 library on existential rules [1] has finally landed last week. The definitions are (and were) based on infinite lists and trees but now do a better job at hiding the implementation details. For example, before I was messing with indices and addresses a lot to talk about list and tree members. This is now abstracted away (for the most part). While being a huge quality of life improvement for myself, it also makes many theorem statements significantly more readable :)

[1] https://github.com/monsterkrampe/Existential-Rules-in-Lean

GitHub - monsterkrampe/Existential-Rules-in-Lean: This repo contains formalizations around Existential Rules (aka. Tuple-Generating Dependencies) with disjunctions and the Chase algorithm. Mostly this will be about (basics of) my own formal works.

This repo contains formalizations around Existential Rules (aka. Tuple-Generating Dependencies) with disjunctions and the Chase algorithm. Mostly this will be about (basics of) my own formal works....

GitHub
Philip ZuckerFeb 2
[New Blog Post] Calling Lean Functions As Python Functions https://www.philipzucker.com/leancall/ #lean4 #python
Calling Lean Functions As Python Functions

I think Lean is neat.

Hey There Buddo!
shnarazk   🎄Jan 31

lean-tui 0.0.10 does not work. reverted to 0.0.9.

  • no --version yet
  • needs to add an extra dependency to each(?!) repository now

😑 #lean4

TariqJan 21

You don't need a PhD to start writing simple maths proofs in Lean.

This beginner-friendly course gets you started making your first steps.

https://www.amazon.com/dp/B0DWHS1RDJ

#maths #leanprover #proofassistants #lean4

vgarzareynaJan 19

I need a little help with a Lean proof. I'm trying to learn the syntax/tactics available in lean so I decided to try to prove the following theorem (as explicitly as I can).

theorem succ_odd_is_even (h : Odd n) : Even n.succ

right now I think I almost got it, but I got to the point where idk how to continue without using "grind", and "apply?" is not showing me any useful hints.

this is the tactic state:
n : Nat
h : ∃ K, n = 2 * K + 1
k : Nat
⊢ n = 2 * k + 1

#lean4 #leanprover