Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > sci.physics > #894003

L∃∀n prover does embrace AI Fusion (Re: Semantic Indexing: Scaling Proofs as Programs)

Show all headers | View raw

Hi,

Maybe somebody should tell Macron that there is
a Stargate project now. Instead using TurdPit for
human Trial & Error of chipmunks, Lean prover from
Microsoft has some interesting projects actually:

LeanDojo (Stanford / Meta AI collaborators)
Turns L∃∀n into a reinforcement learning environment for LLMs.
Train AI to interact with the L∃∀n prover like a human.
https://github.com/lean-dojo/LeanDojo

ProverBot9001
A transformer-based model that learns to generate
L∃∀n proofs. Focused on learning from L∃∀n's mathlib
and applying fine-tuned techniques.
Uses encoder-decoder LLMs and proof search.

Autoformalization of Math
Stanford, OpenAI, and DeepMind folks have tried
autoformalizing math text (LaTeX or natural language)
into L∃∀n. Ongoing effort to turn the “arxiv math paper” →
“Lean formal proof” into a pipeline.

GPT Agents for Lean
Some work on tool-augmented LLMs that run L∃∀n, read
the output, and continue the proof.
Think: GPT as an agent in a loop with L∃∀n — tries
a tactic, checks result, adapts.
Experimental, but shows promise.

Mathlib + tactic-state datasets
Hugely valuable structured data from mathlib for
training and evaluating AI models. Models can learn
by seeing before-and-after proof states. Some teams
are working on LLMs that can select the next tactic
by learning from these states.

Have Fun!

Bye

Mild Shock schrieb:
> Hi,
> 
> Maybe they should double check what
> modern compilers do or what modern IDEs
> to in object orient programming languages.
> 
> How it started:
> 
> How to Make Ad Hoc Proof Automation Less Ad Hoc
> https://people.mpi-sws.org/~beta/lessadhoc/
> 
> How its going:
> 
> Optimizing Canonical Structures
> https://inria.hal.science/hal-05148851v1/document
> 
> The original paper termed canonical structures,
> it has a nice visa à visa. “Type Class” Programming
> versus “Logic” Programming,
> 
> giving it a less functional programming
> spin. But hell wasn't there Prolog++ already
> in the past?
> 
> The newest paper shows new style of research,
> citing garbage tickets from TurdPit inside
> a paper, and just listing some further
> 
> untested and shallow research Turds. Kind
> of institutionalize Trial & Error. They could
> equally well shoot their own Foot and
> 
> then jump in circles.
> 
> Bye

Back to sci.physics | Previous | Next — Previous in thread | Find similar

Thread

Semantic Indexing: Scaling Proofs as Programs Mild Shock <janburse@fastmail.fm> - 2025-07-16 11:56 +0200
  L∃∀n prover does embrace AI Fusion (Re: Semantic Indexing: Scaling Proofs as Programs) Mild Shock <janburse@fastmail.fm> - 2025-07-16 12:10 +0200

csiph-web