Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > sci.physics > #895466
| From | Mild Shock <janburse@fastmail.fm> |
|---|---|
| Newsgroups | sci.physics |
| Subject | Kaffeekränzchen mit ChatGPT (Re: L∃∀n prover does embrace AI Fusion) |
| Date | 2026-03-17 18:25 +0100 |
| Message-ID | <10pc2r5$6ics$2@solani.org> (permalink) |
| References | <1057svq$2a87p$3@solani.org> <1057tr7$2a8ld$4@solani.org> |
A1 = 18 A2 = 63 A3 = 51 A4 = 17 A5 = 54 A6 = 23 Kaffeekränzchen mit ChatGPT. So weit hat es die Menschheit gebracht. Jens Kallup schrieb: > F1: 2 4 6 8 19 12 14 16 = ? > A1: > > > F2: 87 83 79 75 71 67 = ? > A2: > > > F3: 99 105 83 89 67 73 = ? > A3: > > > F4: 2 4 3 6 5 10 9 18 = ? > A4: > > > F5: 33 34 36 39 43 48 = ? > A5: > > > F6: 2 3 5 7 11 13 17 19 = ? > A6: Mild Shock schrieb: > 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 | Find similar
Kaffeekränzchen mit ChatGPT (Re: L∃∀n prover does embrace AI Fusion) Mild Shock <janburse@fastmail.fm> - 2026-03-17 18:25 +0100
csiph-web