From: janburse@fastmail.fm   
      
   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   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)