I'm trying out Aristotle and Lean Copilot for formalizing and proving theorems, and, so far, Aristotle feels way more powerful. Lean Copilot's suggestions aren't always right. Aristotle, on the other hand, can bring in previous lemmas, figure out missing hypotheses, and so on –besides, of course, finishing the proofs themselves.

Disclaimer: this is probably mostly down to the underlying model: Aristotle uses a specialized in-house model (within an agentic architecture), while Lean Copilot is using a more general-purpose one (and not a particularly strong one, at least in my setup... DeepSeek-R1, I think).

#lean #theoremproving #aristotle

Hey algorithm, please help me get exposed to people who are interested in type theory, theorem proving and Principia Mathematica. I'm formalizing Principia Mathematica in Rocq.

https://github.com/MudroadWhite/Neo-Principia/

If you want to tame the monster created a century ago by Bertrand Russell, here's your chance to pet the dragon. *pat pat* Comment if you are interested in!

#RocqProver #TheoremProving #formalverification #AI4Math #typetheory #PrincipiaMathematica

https://lispy-gopher-show.itch.io/lispmoo2/devlog/1481398/homespun-acl2-handler-bind-condition-handling

#acl2 simple introduction to acl2 for the #commonLisp inclined.

loop$, apply$, thms oh my.

In particular, I implement a model of a simple case of the common lisp condition system that is directly compatible with both ansi common lisp and acl2. (a computational logic for applicative common lisp).

#firstOrderLogic #theoremProving #programming #logic #example

Technically this is in support of my lisp / moo compatibility layer but I am not going to beleaguer the tag.

RE: https://floss.social/@alcinnz/116319031843948749

About programming explicitly, the US tax code implicitly, and the difficulty of translating natural and legal language into simple… anything, really; code, webpages, outcomes.

Waving my hands at *two* things I know nothing about: has anyone translated any tax code into a theorem prover? #TheoremProving

Want to learn more about the latest developments on using AI and (interactive) theorem proving in Mathematics? Wait no longer!

We have a great line-up of speakers at our online Workshop on AI and Theorem Provers in Mathematics. The workshop will be held online from 8th to 10th of April and attendance is free (registration required). For more details, visit the workshop website: https://aitpm.github.io/

#math #itp #theoremProving #isabelleHOL #lean #llm #ai #formal_mehods #agda #hol #mathematics

Terminal now can help you with formal proofs and theorem provers 🤯

📐 **lean-tui** — A TUI for visualizing Lean programs and proofs

💯 Live proof trees, data/effect flow views & real-time updates from your editor

🦀 Written in Rust & built with @ratatui_rs

⭐ Source: https://codeberg.org/wvhulle/lean-tui

#rustlang #ratatui #tui #lean #theoremproving #cli #devtools #terminal