Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

---

Topics:

• AI-discovered proof on psi-integrals (with Lean formalizat.) (34 messages, latest: Dec 20 2025 at 12:48)
• Seed Prover 1.5 proves 11 / 12 Putnam 2025 in 9 hours (16 messages, latest: Dec 20 2025 at 08:18)
• Discussion of Gödel's Poetry: Open source, recursive prover (1 message, latest: Dec 17 2025 at 16:34)
• Prove linear algebra by Aristotle (17 messages, latest: Dec 15 2025 at 16:20)
• Discussion: AI-written mathematical proofs (69 messages, latest: Dec 15 2025 at 14:36)
• Track checking function in Pantograph (31 messages, latest: Dec 15 2025 at 07:49)
• Porting between Lean versions (4 messages, latest: Dec 12 2025 at 09:58)
• the-story-of-erdos-problem-1026 (11 messages, latest: Dec 11 2025 at 18:30)
• PutnamBench (84 messages, latest: Dec 10 2025 at 19:13)
• Discussion: Goedel-Prover-V2: A new SOTA model (51 messages, latest: Dec 10 2025 at 12:59)
• ashme/aime in lean in < 10GB weights ? (5 messages, latest: Dec 09 2025 at 19:58)
• Tool to verify a solution solves the actual problem? (27 messages, latest: Dec 09 2025 at 08:44)
• Planner + Generator Trend in Recent-ish NTP models (6 messages, latest: Dec 08 2025 at 14:46)
• best open weight lean4 autoformalization tool ? (4 messages, latest: Dec 08 2025 at 01:17)
• What tool do you use to apply LLMs for Lean? (2 messages, latest: Dec 07 2025 at 07:39)
• Erdos 124 AI Solution (26 messages, latest: Dec 05 2025 at 19:38)
• Aristotle writing rust? (20 messages, latest: Dec 05 2025 at 12:54)
• Theorem Happy Hour @ NeurIPS 2025 (1 message, latest: Dec 04 2025 at 18:10)
• Can Lean REPL/LeanInteract be sandboxed? (3 messages, latest: Dec 04 2025 at 13:53)
• Aristotle achieves SOTA 96.8% proof generation on VERINA (2 messages, latest: Dec 04 2025 at 08:35)
• Aleph Prover by Logical Intelligence (22 messages, latest: Dec 03 2025 at 18:48)
• Kaggle, 38/50 already via open models, $2M prize fund (6 messages, latest: Dec 02 2025 at 23:03)
• Showcase: Smoothstep-Based $G^\infty$ curve (2 messages, latest: Dec 02 2025 at 12:04)
• any "open training data; open training code" IMO solvers ? (20 messages, latest: Dec 02 2025 at 08:34)
• Releasing LeanDojo (77 messages, latest: Dec 01 2025 at 11:46)
• LLM assistant for Lean (1 message, latest: Dec 01 2025 at 00:09)
• Can this GPT 5.1 be simplified? (7 messages, latest: Nov 30 2025 at 21:00)
• AlphaEvolve (23 messages, latest: Nov 29 2025 at 21:49)
• DeepSeekMath_V2 (15 messages, latest: Nov 29 2025 at 02:32)
• Chatting at NIPS (1 message, latest: Nov 27 2025 at 01:15)
• How have you guys found GPT 5? (52 messages, latest: Nov 25 2025 at 23:34)
• Gemini 3 pro performance on formal benchmarks (6 messages, latest: Nov 25 2025 at 23:29)
• lean-lsp-mcp has now integrated Lean Finder (7 messages, latest: Nov 25 2025 at 18:46)
• Any Gemini 3 experiences? (11 messages, latest: Nov 24 2025 at 15:28)
• Domains for controlled AI setups (3 messages, latest: Nov 20 2025 at 16:23)
• AlphaProof Paper (discussion) (19 messages, latest: Nov 20 2025 at 05:24)
• Micro Mathlib (18 messages, latest: Nov 19 2025 at 23:05)
• Thesis directions in ML4TP (1 message, latest: Nov 18 2025 at 13:57)
• Large scale verification with latest lean version (v4.24) (4 messages, latest: Nov 16 2025 at 23:03)
• Lean Datasets for AI Blog (1 message, latest: Nov 14 2025 at 14:23)
• formal-imo (discussion) (8 messages, latest: Nov 12 2025 at 23:13)
• AlphaProof trusted tester programme (discussion) (4 messages, latest: Nov 12 2025 at 21:38)
• Blind Speculation about IMO 2025 (62 messages, latest: Nov 12 2025 at 16:55)
• LeanDojo tracing and caching (7 messages, latest: Nov 07 2025 at 21:19)
• Danger of Autoformalizers (e.g. Gauss) (54 messages, latest: Nov 07 2025 at 15:47)
• Ensembling with NTP Models (2 messages, latest: Nov 07 2025 at 01:13)
• BFS-Prover-V2 (21 messages, latest: Nov 07 2025 at 00:16)
• Hilbert Agent (14 messages, latest: Nov 05 2025 at 14:35)
• Claude Code (20 messages, latest: Nov 03 2025 at 20:26)
• Assessing the adequacy of an LLM-generated reasoning trace (1 message, latest: Nov 02 2025 at 07:25)
• RFC: Thoughts on a Lean4 model context protocol (MCP) SDK? (19 messages, latest: Oct 30 2025 at 21:07)
• ProofOptimizer (4 messages, latest: Oct 28 2025 at 13:45)
• theoretical computer science / STOC automated reviews (4 messages, latest: Oct 27 2025 at 14:02)
• Survey on AI Tools in Mathematics (1 message, latest: Oct 26 2025 at 02:56)
• Lean Skill for Claude Code (28 messages, latest: Oct 24 2025 at 23:30)
• Seems LLM works well on modular structure (6 messages, latest: Oct 24 2025 at 16:15)
• Progress in Guaranteed Safe AI Newsletter (1 message, latest: Oct 22 2025 at 02:43)
• Judging formalization (11 messages, latest: Oct 18 2025 at 23:08)
• LLM-powered tactics (2 messages, latest: Oct 14 2025 at 12:01)
• Sign Up for the Aristotle API! (20 messages, latest: Oct 09 2025 at 07:28)
• COLM 2025 (1 message, latest: Oct 08 2025 at 19:45)
• Aristotle report (1 message, latest: Oct 08 2025 at 18:51)
• FormalML benchmark (1 message, latest: Oct 06 2025 at 09:20)
• Checking large AI generated projects (23 messages, latest: Oct 05 2025 at 09:11)
• (deleted) (3 messages, latest: Oct 04 2025 at 09:58)
• Towards human AI collaboration (5 messages, latest: Oct 01 2025 at 00:44)
• Crossposting AI for formal math job ad at Mistral AI (1 message, latest: Sep 29 2025 at 14:14)
• Worry: AI doing most of the coding but no real acceleration (9 messages, latest: Sep 28 2025 at 15:48)
• Wrong informal proof by AI (15 messages, latest: Sep 26 2025 at 20:02)
• DeepSeek-Prover V2 (259 messages, latest: Sep 26 2025 at 18:13)
• Role reversal (31 messages, latest: Sep 25 2025 at 19:46)
• gpt-5-Codex is available on openrouter (14 messages, latest: Sep 25 2025 at 16:26)
• Math, Inc, and Gauss discussion (88 messages, latest: Sep 25 2025 at 15:36)
• DeepMind and Navier Stokes (23 messages, latest: Sep 24 2025 at 00:37)
• How close are we to semi-automated Mathlib bumping? (44 messages, latest: Sep 23 2025 at 23:17)
• Artificial Algorithms (58 messages, latest: Sep 23 2025 at 09:26)
• Theorem proving olympiad (10 messages, latest: Sep 19 2025 at 12:51)
• Seed Prover Achieves Silver-Level Score at IMO 2025 (169 messages, latest: Sep 19 2025 at 07:13)
• SorryDB project (11 messages, latest: Sep 17 2025 at 10:06)
• Monte Carlo tree search (9 messages, latest: Sep 17 2025 at 01:53)
• AlphaGeometry doesn't have a secure foundation (26 messages, latest: Sep 17 2025 at 01:50)
• Kimina Lean Server (2 messages, latest: Sep 16 2025 at 17:05)
• codex (1 message, latest: Sep 12 2025 at 06:01)
• Agora (12 messages, latest: Sep 10 2025 at 19:07)
• Performance of models for formalisation (3 messages, latest: Sep 04 2025 at 03:52)
• AITP 2025 (3 messages, latest: Sep 03 2025 at 14:18)
• Autoformalisation (23 messages, latest: Sep 03 2025 at 06:12)
• Context Rot in MLTP (3 messages, latest: Aug 31 2025 at 15:24)
• DeepWiki for searching Mathlib (1 message, latest: Aug 22 2025 at 14:12)
• Lean State Search: Search Mathlib theorems with proof states (23 messages, latest: Aug 22 2025 at 02:00)
• we should collaborate (2 messages, latest: Aug 13 2025 at 12:09)
• DSL for theorem proving? (16 messages, latest: Aug 11 2025 at 00:55)
• Harmonic: IMO Livestream (56 messages, latest: Aug 07 2025 at 02:28)
• Guarding against exploits in AI code (37 messages, latest: Aug 02 2025 at 00:07)
• PSA: Lean MCP tools breakage with FastMCP (3 messages, latest: Aug 01 2025 at 06:41)
• Inference providers no longer hosting Lean 4 models (10 messages, latest: Jul 30 2025 at 16:20)
• MCP Tools for LLMs and Agentic Mathematics (129 messages, latest: Jul 30 2025 at 07:51)
• Delta Prover (29 messages, latest: Jul 26 2025 at 05:34)
• Good conferences and workshops to attend (5 messages, latest: Jul 24 2025 at 15:10)
• MATH-AI workshop @ NeurIPS 2025 (1 message, latest: Jul 23 2025 at 14:44)
• Verified Coding Agents (1 message, latest: Jul 22 2025 at 20:53)
• Code for turning goal state strings into theorem statements (2 messages, latest: Jul 21 2025 at 19:18)
• Lean Copilot setup issue: no .Olean file created (1 message, latest: Jul 21 2025 at 19:14)
• OpenAI IMO Gold Medal (48 messages, latest: Jul 21 2025 at 17:44)
• Provably-Correct Vibe Coding (8 messages, latest: Jul 16 2025 at 04:51)
• Cases/induction in Single-Step Tactic generation LLM (3 messages, latest: Jul 13 2025 at 09:51)
• ICML2025 (7 messages, latest: Jul 12 2025 at 20:06)
• Gemini 2.5 Pro 06/05 (15 messages, latest: Jul 10 2025 at 17:46)
• Tool for cleaning / compressing proofs? (6 messages, latest: Jul 09 2025 at 14:08)
• Reproducing LEGO Prover (1 message, latest: Jul 07 2025 at 02:25)
• Dataset to rule them all? (4 messages, latest: Jul 06 2025 at 23:22)
• Building an Autoformalizer on Analysis (2 messages, latest: Jul 05 2025 at 17:04)
• ✔ Executing Conv and Calc in Pantograph (6 messages, latest: Jul 01 2025 at 22:47)
• REPL: automated incremental state reuse across commands (10 messages, latest: Jun 30 2025 at 19:13)
• Better way for tracing tactic states (9 messages, latest: Jun 29 2025 at 22:40)
• Claude 4 agent in VS Code (6 messages, latest: Jun 28 2025 at 13:27)
• LeanTool feature: Sorry Hammer (2 messages, latest: Jun 27 2025 at 09:39)
• AI tutorial for LEAN beginner (24 messages, latest: Jun 22 2025 at 19:07)
• Proof or Bluff (51 messages, latest: Jun 22 2025 at 05:33)
• Autoformalization of the probabilistic abc-conjecture (36 messages, latest: Jun 18 2025 at 12:13)
• Illusion of Thinking (12 messages, latest: Jun 13 2025 at 00:25)
• Tool for Lean code verify (5 messages, latest: Jun 09 2025 at 04:04)
• Current state of AI for Mathematics and what could come n… (61 messages, latest: Jun 08 2025 at 22:17)
• System card: Claude Opus 4 & Claude Sonnet 4 (10 messages, latest: Jun 05 2025 at 09:54)
• I was pleasantly surprised by DeepSeek (13 messages, latest: Jun 02 2025 at 11:17)
• Automated theorem proving as program synthesis? (6 messages, latest: Jun 02 2025 at 11:12)
• A more robust RL pipeline? (21 messages, latest: May 26 2025 at 20:28)
• Crowdsourcing ATP (4 messages, latest: May 26 2025 at 17:46)
• First impressions from using Claude 4 Opus and Sonnet (47 messages, latest: May 26 2025 at 14:26)
• A (semi)-autoformalization challenge: 650=>448 (19 messages, latest: May 24 2025 at 19:41)
• CLEVER: A Benchmark for Verified Code Generation in Lean (1 message, latest: May 23 2025 at 21:07)
• Diverse Inference and Verification for Advanced Reasoning (9 messages, latest: May 23 2025 at 20:24)
• A proposal for Safe and Hallucinatio-free coding AI (28 messages, latest: May 23 2025 at 20:09)
• What queries do you type in Moogle/LeanSearch? (7 messages, latest: May 20 2025 at 18:13)
• Extracting full goal from REPL with type information (8 messages, latest: May 17 2025 at 22:44)
• Tools for semi-automated line-by-line formalization (16 messages, latest: May 17 2025 at 17:27)
• Incentives & sorry-filling leaderboard (101 messages, latest: May 15 2025 at 07:22)
• Hard proof-based auto-formalization benchmark (30 messages, latest: May 13 2025 at 00:03)
• ✔ A dataset of proofs for 20 IMO problems and extracted l… (3 messages, latest: May 09 2025 at 10:45)
• Beyond TP: Formal Problem-Solving (6 messages, latest: May 09 2025 at 03:02)
• setting up leantool in roo-code (30 messages, latest: May 07 2025 at 14:49)
• ✔ DeepSeek-Prover-V2 : how to get started (13 messages, latest: May 07 2025 at 03:51)
• DeepSeek-Prover V2 TODO List (12 messages, latest: May 05 2025 at 14:03)
• request for help on the REPL (76 messages, latest: May 05 2025 at 09:27)
• Building up Lean.Expr's (17 messages, latest: May 04 2025 at 21:23)
• Talk: Preparing for the next stage in autoformalization (23 messages, latest: May 02 2025 at 01:45)
• ProverBench (53 messages, latest: May 02 2025 at 00:01)
• ✔ Lean Zulip Chat Dataset (65 messages, latest: May 01 2025 at 19:40)
• ✔ Tool searching for similar Mathlib theorems to natural … (4 messages, latest: Apr 29 2025 at 15:47)
• CombiBench benchmark (1 message, latest: Apr 28 2025 at 22:31)
• Introducing APE-Bench I (5 messages, latest: Apr 28 2025 at 04:07)
• Concurrency and batch processing in pantograph (12 messages, latest: Apr 26 2025 at 02:39)
• Serverless Pantograph on Morph Cloud (1 message, latest: Apr 26 2025 at 01:49)
• Auto-formalization for the working mathematician (6 messages, latest: Apr 24 2025 at 20:38)
• Simons Institute for the Theory of Computing and SLMath Join (2 messages, latest: Apr 24 2025 at 06:58)
• miniCTX (8 messages, latest: Apr 24 2025 at 01:26)
• ICLR 2025 Posters (1 message, latest: Apr 23 2025 at 23:44)
• Kimina Prover Preview Demo (6 messages, latest: Apr 23 2025 at 17:16)
• ✔ error installing pantograph(windows) (28 messages, latest: Apr 23 2025 at 01:31)
• How to use the REPL from within python? (45 messages, latest: Apr 21 2025 at 20:12)
• Lean-based advanced mathematics benchmark (8 messages, latest: Apr 16 2025 at 12:31)
• a question about premise retrieval using lean dojo (9 messages, latest: Apr 16 2025 at 11:11)
• ABEL (14 messages, latest: Apr 14 2025 at 22:15)
• Interacting with Lean 4 (42 messages, latest: Apr 14 2025 at 18:21)
• Embedder for Lean+NL (3 messages, latest: Apr 10 2025 at 07:19)
• Owlgebra - automated proof discovery (21 messages, latest: Apr 08 2025 at 13:54)
• using/training llms to call powerful tactics (10 messages, latest: Apr 07 2025 at 18:28)
• Talk on AlphaProof (1 message, latest: Apr 02 2025 at 12:25)
• VSCode plugin that connects an agent to the tactic state (11 messages, latest: Apr 01 2025 at 14:51)
• benchmarking Gemini 2.5 pro (17 messages, latest: Apr 01 2025 at 12:40)
• Does llmstep project still work? (3 messages, latest: Mar 26 2025 at 13:35)
• Lean Verifier ie Formal verification of ML Models (5 messages, latest: Mar 26 2025 at 13:30)
• ATP-related tactics VS AI automation (9 messages, latest: Mar 24 2025 at 13:12)
• LeanCopilot Setup (9 messages, latest: Mar 18 2025 at 12:33)
• I see - but it seems to me that Lean Copilot is only supp… (1 message, latest: Mar 14 2025 at 22:05)
• build issues: A dataset of proofs for 20 IMO problems … (21 messages, latest: Mar 14 2025 at 10:37)
• A dataset of proofs for 20 IMO problems and extracted lemmas (11 messages, latest: Mar 12 2025 at 04:50)
• ✔ How to get explicit types printed in the inforview (12 messages, latest: Mar 06 2025 at 13:44)
• Cap set improvement (4 messages, latest: Mar 06 2025 at 07:30)
• Do AI Models Struggle with Combinatorics? (4 messages, latest: Mar 05 2025 at 12:44)
• Piecework jobs creating Lean 4 training corpora for LLMs (3 messages, latest: Feb 27 2025 at 03:14)
• Goedel-Prover (5 messages, latest: Feb 26 2025 at 11:08)
• How to start as a non mathematician (3 messages, latest: Feb 26 2025 at 04:16)
• A simple AI benchmark problem: Spearman correlation = 0.5 (16 messages, latest: Feb 19 2025 at 18:48)
• Lean Scribe: Render and run context-rich prompts in VSCode (1 message, latest: Feb 18 2025 at 18:09)
• Which Python <–> Lean interfaces exist? (37 messages, latest: Feb 15 2025 at 17:20)
• LLMs for Mathematics (6 messages, latest: Feb 13 2025 at 07:32)
• FVAPPS discussion (26 messages, latest: Feb 11 2025 at 19:55)
• Lean 4 gym (38 messages, latest: Feb 11 2025 at 00:04)
• itp-interface and proof-wala (1 message, latest: Feb 10 2025 at 23:55)
• IMO results from Google DeepMind (179 messages, latest: Feb 09 2025 at 14:33)
• Simple but hard puzzler for LLMs (88 messages, latest: Feb 05 2025 at 19:33)
• Current state of end-user tools (71 messages, latest: Feb 01 2025 at 16:02)
• FrontierMath: Formalising Benchmark Problems (16 messages, latest: Feb 01 2025 at 13:44)
• AI on Lean workshop names (1 message, latest: Jan 30 2025 at 14:36)
• on doing RL against Lean R1-style (1 message, latest: Jan 29 2025 at 20:13)
• LLMs for (Informal) Math (1 message, latest: Jan 29 2025 at 20:09)
• Building proof trees from tactic proofs (15 messages, latest: Jan 29 2025 at 09:04)
• DeepSeek-Prover-V1.5 (10 messages, latest: Jan 29 2025 at 05:09)
• Announcing a project: lean-mine (2 messages, latest: Jan 28 2025 at 06:04)
• leanclient: Interact with Lean from Python via the LSP (17 messages, latest: Jan 27 2025 at 14:42)
• The use of tactics in the creation of data sets (11 messages, latest: Jan 26 2025 at 19:18)
• Open open benchmarks (10 messages, latest: Jan 26 2025 at 18:31)
• Automated Math Prove Synthesizer without Deep Learning (9 messages, latest: Jan 26 2025 at 04:49)
• "Humanity's Last Exam" (1 message, latest: Jan 24 2025 at 00:56)
• Questions to the ML community (62 messages, latest: Jan 22 2025 at 12:02)
• Best open-source/open-access models for proving Lean thms? (7 messages, latest: Jan 20 2025 at 21:13)
• LeanAgent (129 messages, latest: Jan 12 2025 at 06:27)
• LeanUniverse (6 messages, latest: Jan 12 2025 at 02:11)
• JMM AI4Math Meet-up (11 messages, latest: Jan 10 2025 at 05:37)
• AI for Math Fund (1 message, latest: Jan 09 2025 at 18:04)
• Is restricting the set of tactics a good idea for RL? (36 messages, latest: Jan 08 2025 at 15:51)
• ✔ help using PyPantograph (8 messages, latest: Jan 05 2025 at 15:49)
• Formal Mathematical Reasoning: A New Frontier in AI (1 message, latest: Dec 24 2024 at 16:40)
• FrontierMath, a benchmark for evaluating advanced mathema… (53 messages, latest: Dec 23 2024 at 19:25)
• is the AI for ITP community sleeping on o1? (13 messages, latest: Dec 23 2024 at 11:37)
• OpenAI's Reinforcement Fine-Tuning Research Program (2 messages, latest: Dec 18 2024 at 18:22)
• large formal math dataset by Numina (6 messages, latest: Dec 18 2024 at 03:51)
• ProofNet fix (17 messages, latest: Dec 17 2024 at 13:01)
• Pantograph (52 messages, latest: Dec 12 2024 at 01:26)
• NeurIPS 2024 (7 messages, latest: Dec 07 2024 at 12:07)
• Is Autoformalization needed? (28 messages, latest: Dec 07 2024 at 09:49)
• Can lean instantiate a state? (5 messages, latest: Dec 05 2024 at 08:15)
• Advice on using PDFs with LLMs (e.g. math papers)? (7 messages, latest: Dec 03 2024 at 15:31)
• Autoformalization of Coding Problems (21 messages, latest: Dec 03 2024 at 10:51)
• chart minif2f progress over time (3 messages, latest: Dec 02 2024 at 22:27)
• Workshop on Theorem Proving and Machine Learning (3 messages, latest: Nov 26 2024 at 22:54)
• AlphaProof team on podcast (1 message, latest: Nov 18 2024 at 02:07)
• Lean benchmarks for modern (opaque) LLMs (13 messages, latest: Nov 07 2024 at 16:21)
• Installing Lean Copilot but have "git" problem (9 messages, latest: Nov 06 2024 at 03:26)
• Combinatorics Benchmark in Lean 4 (1 message, latest: Nov 03 2024 at 01:56)
• Proper LLM Lean4 Integration with recursive checks for error (16 messages, latest: Oct 31 2024 at 07:05)
• ICLR 2025 Submissions (18 messages, latest: Oct 28 2024 at 23:27)
• Proof Scaling Meeting in Berkeley (2 messages, latest: Oct 28 2024 at 19:15)
• ✔ Output of LLMs in tactic generation (8 messages, latest: Oct 27 2024 at 22:45)
• InternLM2.5-StepProver (7 messages, latest: Oct 24 2024 at 02:23)
• Areas of math where synthetic generation of problems of v… (10 messages, latest: Oct 21 2024 at 23:51)
• MATH AI (1 message, latest: Oct 19 2024 at 14:34)
• Keep AI theorem provers up-to-date (17 messages, latest: Oct 18 2024 at 14:11)
• AI / ML for the Equational Theories Project? (1 message, latest: Oct 13 2024 at 14:48)
• Transpiling code (5 messages, latest: Sep 30 2024 at 14:21)
• OpenAI "Learning to Reason with LLMs" (59 messages, latest: Sep 21 2024 at 07:25)
• LLMLean, anyone using it? (26 messages, latest: Sep 18 2024 at 08:53)
• ChatGPT can help translate between Coq and Lean (20 messages, latest: Sep 16 2024 at 13:08)
• o1 (1 message, latest: Sep 16 2024 at 11:03)
• AITP 2024 (6 messages, latest: Sep 12 2024 at 10:57)
• Neural symbolic summer school talk (1 message, latest: Sep 06 2024 at 10:53)
• Aristotle (58 messages, latest: Sep 03 2024 at 23:41)
• Linear logic and game semantics (4 messages, latest: Sep 03 2024 at 07:33)
• Three meetings on AI/ML for Math/Theorem Proving this week (1 message, latest: Sep 01 2024 at 14:30)
• Anyone interested in a full paper list of AI mathematics? (13 messages, latest: Aug 19 2024 at 00:30)
• AI Program Generation and Verification in Lean (10 messages, latest: Aug 14 2024 at 18:17)
• $50,000 Prize in the Mathematics of Artificial Intelligence (1 message, latest: Aug 09 2024 at 02:27)
• The set of all even numbers (14 messages, latest: Aug 08 2024 at 11:06)
• ICML (17 messages, latest: Aug 08 2024 at 10:55)
• AI/ML tools for Lean (24 messages, latest: Aug 07 2024 at 14:07)
• Reinforcement learning for solving a single theorem (11 messages, latest: Aug 05 2024 at 14:30)
• InternLM-Step-Prover and Lean-Github (9 messages, latest: Jul 25 2024 at 14:17)
• Is Autoformalization just a special case of semantic parsing (22 messages, latest: Jul 24 2024 at 10:53)
• AIMO at IMO 2024 (2 messages, latest: Jul 20 2024 at 14:07)
• Evaluation of Formal proofs (11 messages, latest: Jul 19 2024 at 11:13)
• Status of leanprover-community/llm (7 messages, latest: Jul 16 2024 at 04:01)
• AIPS (4 messages, latest: Jul 14 2024 at 23:57)
• TheoremLlama (6 messages, latest: Jul 14 2024 at 21:43)
• Harmonic (1 message, latest: Jul 10 2024 at 11:11)
• yes (1 message, latest: Jul 08 2024 at 23:07)
• AI for Mathematics (AI4Math) Papers (1 message, latest: Jun 30 2024 at 15:57)
• Percentage of Mizar theorems solved (14 messages, latest: Jun 27 2024 at 18:02)
• New paper: Magnushammer (28 messages, latest: Jun 27 2024 at 08:04)
• GPT generated theorem descriptions. (37 messages, latest: Jun 26 2024 at 21:05)
• plaintext/AI-readable lean4 syntax guide (5 messages, latest: Jun 25 2024 at 23:14)
• ARC Prize (16 messages, latest: Jun 18 2024 at 21:34)
• DafnyBench (3 messages, latest: Jun 17 2024 at 03:47)
• benchmarks (14 messages, latest: Jun 15 2024 at 09:04)
• DeepSeek-Prover (78 messages, latest: Jun 11 2024 at 12:04)
• Lean Workbook: A large-scale Lean formalized problem set (8 messages, latest: Jun 09 2024 at 06:30)
• Paper: Autoformalizing Euclidean Geometry (4 messages, latest: May 28 2024 at 21:02)
• InternLM-Math-Plus (3 messages, latest: May 28 2024 at 04:07)
• Synthetic dataset generation (10 messages, latest: May 24 2024 at 18:52)
• LLM generation of proofs in FLT project? (2 messages, latest: May 06 2024 at 15:11)
• EvoGPT-f Lean Benchmark (8 messages, latest: Apr 26 2024 at 17:18)
• NASEM webinar 4/23-4/25 (14 messages, latest: Apr 24 2024 at 17:00)
• LeanCopilot (124 messages, latest: Apr 22 2024 at 19:11)
• Python library for lean3 (5 messages, latest: Apr 20 2024 at 16:36)
• A Survey on Deep Learning for Theorem Proving (4 messages, latest: Apr 20 2024 at 15:26)
• AI Mathematical Olympiad (2 messages, latest: Apr 08 2024 at 10:33)
• New paper: Use Lean to help with natural language reasoning (1 message, latest: Apr 07 2024 at 02:54)
• lean copilot problem (1 message, latest: Apr 01 2024 at 17:21)
• Testimonials (7 messages, latest: Mar 25 2024 at 18:33)
• AlphaGeometry (64 messages, latest: Mar 13 2024 at 22:40)
• Call for Papers - DAV 2024 (1 message, latest: Mar 11 2024 at 18:57)
• ProofNet ported in Lean 4 (4 messages, latest: Mar 06 2024 at 05:19)
• Seeking mentorship (3 messages, latest: Mar 04 2024 at 10:25)
• dreamcoder (33 messages, latest: Mar 02 2024 at 19:26)
• ML on tactics vs terms? (40 messages, latest: Feb 27 2024 at 12:29)
• LeanGPT (30 messages, latest: Feb 19 2024 at 23:08)
• Announcing Graph2Tac, a prover based on Tactician's new API (29 messages, latest: Feb 10 2024 at 22:23)
• Store LeanCopilot cache elsewhere (5 messages, latest: Feb 07 2024 at 21:34)
• Theorem proving in artificial neural networks: new fronti… (2 messages, latest: Jan 23 2024 at 10:33)
• ML for Theorem Proving Tutorial - NeurIPS 2023 (90 messages, latest: Jan 20 2024 at 19:14)
• Lean Chat is publicly available (32 messages, latest: Jan 20 2024 at 12:45)
• Paper feed (26 messages, latest: Dec 29 2023 at 22:27)
• Paper: Enhancing Neural Theorem Proving through Data Augm… (21 messages, latest: Dec 29 2023 at 11:30)
• MATH-AI workshop at NeurIPS (62 messages, latest: Dec 22 2023 at 19:22)
• COPRA (70 messages, latest: Dec 21 2023 at 06:03)
• NeurIPS 2023 meetup (2 messages, latest: Dec 13 2023 at 05:15)
• What's state of public Lean datasets and augmentation? (55 messages, latest: Dec 12 2023 at 02:04)
• hallucination (2 messages, latest: Dec 12 2023 at 01:40)
• Current approach documentation request (4 messages, latest: Dec 09 2023 at 14:27)
• "simplify" tasks rather than "prove a theorem" tasks? (12 messages, latest: Dec 09 2023 at 10:13)
• Making more training data (45 messages, latest: Dec 04 2023 at 17:32)
• morph-prover-v0-7b (7 messages, latest: Dec 02 2023 at 10:06)
• Nougat, academic OCR model from Meta AI (7 messages, latest: Dec 01 2023 at 20:39)
• CoqPilot (1 message, latest: Nov 20 2023 at 13:22)
• OpenAI "make your own GPT" (18 messages, latest: Nov 16 2023 at 18:08)
• Peano (2 messages, latest: Nov 09 2023 at 07:35)
• How to run a simple ATP baseline for Lean (15 messages, latest: Nov 08 2023 at 21:25)
• llmstep (35 messages, latest: Nov 01 2023 at 22:43)
• Paper: MLFMF (10 messages, latest: Oct 30 2023 at 03:49)
• AI + metaprogramming (13 messages, latest: Oct 28 2023 at 20:39)
• Morph Prover v0 7B (39 messages, latest: Oct 25 2023 at 21:40)
• How do mathematicians really feel about AI? (2 messages, latest: Oct 20 2023 at 03:06)
• Llemma (11 messages, latest: Oct 18 2023 at 07:09)
• The personal AI proof engineer (2 messages, latest: Oct 17 2023 at 23:32)
• LeanInfer: Neural Network Inference in Lean 4 (89 messages, latest: Oct 15 2023 at 02:35)
• Lyra (15 messages, latest: Oct 08 2023 at 21:53)
• AI in math reasoning conference (36 messages, latest: Sep 26 2023 at 21:01)
• experiments with copilot (7 messages, latest: Sep 21 2023 at 16:50)
• Semantic Search for Mathematics (79 messages, latest: Sep 04 2023 at 13:57)
• LLM+ITP(+AZ)? (42 messages, latest: Aug 29 2023 at 00:05)
• Paper: Top Down Automated Theorem Proving (17 messages, latest: Aug 24 2023 at 23:18)
• Automatic Theorem Proving Competitions (33 messages, latest: Aug 13 2023 at 23:58)
• DT-Solver (7 messages, latest: Aug 07 2023 at 01:21)
• Looking for help with natural language reasoning task (12 messages, latest: Aug 06 2023 at 22:58)
• Christian Szegedy and Tony Wu joined xAI (27 messages, latest: Jul 21 2023 at 18:59)
• Assistance for GPT-Based Lean research project (9 messages, latest: Jul 16 2023 at 05:04)
• "Will machines change mathematics?" (26 messages, latest: Jun 29 2023 at 06:14)
• server api (12 messages, latest: Jun 19 2023 at 15:31)
• StarCoder (10 messages, latest: Jun 19 2023 at 14:27)
• GPT frontend for mathlib4 (75 messages, latest: Jun 09 2023 at 03:07)
• Using Tree of Thoughts Methodology with Logical Questions (1 message, latest: Jun 06 2023 at 10:13)
• Improving Mathematical Reasoning with Process Supervision (5 messages, latest: Jun 05 2023 at 00:30)
• Tree of GPTs (4 messages, latest: Jun 04 2023 at 07:10)
• Facebook Transcoder for Lean 4 port (7 messages, latest: May 28 2023 at 14:10)
• Minif2f ported to Lean 4 (4 messages, latest: May 28 2023 at 05:20)
• ProofGPT's performance on theorem proving (9 messages, latest: May 27 2023 at 16:10)
• corpus of all rewrites in mathlib4 (24 messages, latest: May 25 2023 at 00:24)
• tokenization of latex for use in sequence models (4 messages, latest: May 22 2023 at 16:20)
• Seeking Insights on Theorem Proving's Role in Enhancing LLM (10 messages, latest: May 20 2023 at 16:23)
• Lean or Isabelle: Which Theorem Proving Tool for LLM? (11 messages, latest: May 20 2023 at 15:35)
• ✔ Random youtube video. (4 messages, latest: May 12 2023 at 02:59)
• REPL for Lean 4 (6 messages, latest: May 03 2023 at 15:35)
• More papers on autoformalization (32 messages, latest: Apr 16 2023 at 13:56)
• Bangalore talk on LLM+ITP (31 messages, latest: Apr 15 2023 at 20:59)
• Crossposting invitation to AI maths study participation (5 messages, latest: Apr 15 2023 at 16:02)
• OCR to LaTeX (7 messages, latest: Apr 11 2023 at 21:20)
• GPT (271 messages, latest: Apr 11 2023 at 08:23)
• sagredo (34 messages, latest: Apr 11 2023 at 03:13)
• Learning new tactics (4 messages, latest: Apr 07 2023 at 02:20)
• April Fool's Day (2 messages, latest: Apr 02 2023 at 21:03)
• stream events (3 messages, latest: Mar 13 2023 at 05:09)
• Baldur: Whole-Proof Generation and Repair with Large Lang… (5 messages, latest: Mar 10 2023 at 23:49)
• Paper: HyperTree Proof Search for Neural Theorem Proving (31 messages, latest: Mar 04 2023 at 19:33)
• Internet Explorer: Targeted Repr Learning on the Open Web (1 message, latest: Mar 04 2023 at 02:07)
• Magnet link to download LLaMA (1 message, latest: Mar 04 2023 at 01:28)
• Comparison among Lean, Coq and HOL (5 messages, latest: Feb 20 2023 at 15:38)
• Getting started with lean-gym (69 messages, latest: Feb 20 2023 at 04:24)
• PACT Paper (39 messages, latest: Feb 17 2023 at 06:41)
• Meta IMO result (64 messages, latest: Jan 10 2023 at 20:01)
• Paper: A Survey of Deep Learning for Mathematical Reasoning (1 message, latest: Jan 03 2023 at 00:01)
• Maintaining Papers with Code for Automated Theorem Proving (46 messages, latest: Dec 22 2022 at 02:12)
• using AI in lean (3 messages, latest: Dec 15 2022 at 09:42)
• ChatGPT / Galactica (24 messages, latest: Dec 03 2022 at 08:23)
• Lean on top of language models? (16 messages, latest: Nov 28 2022 at 19:16)
• Open source for HyperTree paper or Equations? (1 message, latest: Nov 28 2022 at 08:16)
• New paper on arXiv (18 messages, latest: Nov 25 2022 at 19:46)
• meaning of "determine number" (21 messages, latest: Nov 24 2022 at 20:04)
• Other places discussing neural theorem proving (12 messages, latest: Nov 24 2022 at 15:01)
• slides on autoformalisation (1 message, latest: Nov 22 2022 at 14:07)
• Galactica (8 messages, latest: Nov 19 2022 at 16:00)
• Postdoc and Internship positions at IBM Research (1 message, latest: Oct 14 2022 at 22:21)
• Automatically generated lemmas (21 messages, latest: Sep 25 2022 at 08:49)
• Proof repair and constructive math (7 messages, latest: Sep 10 2022 at 11:39)
• AITP 2022 (2 messages, latest: Sep 10 2022 at 10:31)
• What is the AMI project's vision for AI in Lean? (15 messages, latest: Sep 08 2022 at 14:53)
• What is Leo's vision for AI in Lean and the AMI? (4 messages, latest: Jul 23 2022 at 21:11)
• Minerva (4 messages, latest: Jul 02 2022 at 16:27)
• A chat interface for formalizing theorem statements (38 messages, latest: Jun 22 2022 at 19:29)
• Isabelle and neural theorem proving (7 messages, latest: May 27 2022 at 14:49)
• Paper: Autoformalization with Large Language Models (4 messages, latest: May 27 2022 at 14:44)
• IMO Geometry (31 messages, latest: May 22 2022 at 22:44)
• Memorizing transformers (3 messages, latest: May 20 2022 at 18:36)
• MiniF2F (29 messages, latest: Apr 07 2022 at 03:21)
• autoformalization? (15 messages, latest: Mar 11 2022 at 10:53)
• Solving (Some) Formal Olympiad Problems (27 messages, latest: Feb 04 2022 at 00:25)
• New Technologies in Mathematics Seminar at Harvard (21 messages, latest: Jan 29 2022 at 00:07)
• Porting other ITP proofs to Lean (7 messages, latest: Jan 21 2022 at 13:34)
• New paper: transformers for symbolic regression (10 messages, latest: Jan 17 2022 at 20:11)
• "mathematics is infinite" (83 messages, latest: Dec 26 2021 at 19:58)
• Player of Games (Deepmind) (1 message, latest: Dec 08 2021 at 08:00)
• Subgoal Search For Complex Reasoning Tasks (30 messages, latest: Nov 01 2021 at 22:58)
• Parting gift of my notes (1 message, latest: Nov 01 2021 at 13:50)
• HiPPO papers (efficient sequence modeling) (21 messages, latest: Oct 14 2021 at 12:12)
• (no topic) (4 messages, latest: Sep 12 2021 at 19:57)
• Papers on Neural Conjecturing (54 messages, latest: Aug 20 2021 at 02:58)
• Finding similar lemmas (17 messages, latest: Aug 01 2021 at 22:16)
• HOList or Lean? (86 messages, latest: Jul 17 2021 at 08:48)
• Lean gym for Lean 4 (19 messages, latest: Jun 22 2021 at 02:21)
• Math-AI@ICLR (14 messages, latest: Jun 12 2021 at 20:38)
• new results in graph theory. (4 messages, latest: May 26 2021 at 13:24)
• GPT-f paper (88 messages, latest: May 26 2021 at 01:45)
• HOList (188 messages, latest: May 18 2021 at 16:28)
• RL finds counterexamples to open problems in graph theory (2 messages, latest: May 15 2021 at 14:36)
• Generate similar but not equal type (11 messages, latest: May 09 2021 at 10:42)
• Reinforcement learning for ATP (44 messages, latest: May 06 2021 at 22:32)
• gptf generating theorems (6 messages, latest: Apr 29 2021 at 16:01)
• a search engine for Isabelle (1 message, latest: Apr 19 2021 at 21:57)
• universal oracle (29 messages, latest: Apr 19 2021 at 16:17)
• Lean client for Python (148 messages, latest: Apr 16 2021 at 17:25)
• LEO (10 messages, latest: Apr 01 2021 at 14:43)
• Translating between ITPs with machine learning (20 messages, latest: Mar 15 2021 at 05:17)
• Incorporating neural networks into type inhabitation (6 messages, latest: Mar 07 2021 at 14:13)
• AI and artistic taste (28 messages, latest: Mar 01 2021 at 05:10)
• MATH-AI workshop@ICLR (1 message, latest: Feb 09 2021 at 21:21)
• Lean Together 2021 ML talks (7 messages, latest: Jan 05 2021 at 16:24)
• Coq machine learning dataset based on MathComp 1.9.0 (27 messages, latest: Dec 09 2020 at 14:17)
• Tutorial: Abstraction & Reasoning in AI systems: Modern P… (2 messages, latest: Dec 07 2020 at 16:56)
• Post-doc in IHES (3 messages, latest: Nov 27 2020 at 12:53)
• AITP 2020 (161 messages, latest: Sep 21 2020 at 15:05)
• IMO Grand Challenge (17 messages, latest: Sep 17 2020 at 16:24)
• comments (14 messages, latest: Sep 16 2020 at 16:36)
• ML for Lean: How to do it? (132 messages, latest: Aug 24 2020 at 11:58)
• rw_hint (41 messages, latest: Aug 22 2020 at 18:10)
• CoqGym (7 messages, latest: Aug 17 2020 at 17:10)
• Sister Stream on Coq Zulip (1 message, latest: Aug 09 2020 at 14:02)
• CICM Machine Learning and Theorem Proving Session (11 messages, latest: Jul 21 2020 at 23:05)
• Data sets: where to put them? (11 messages, latest: Jul 20 2020 at 09:10)
• Learning based space formatting of proof assistant code (29 messages, latest: Jul 09 2020 at 02:41)
• curmudgeoning (24 messages, latest: Jul 04 2020 at 20:07)
• Paper: Automated Theorem Proving via Interacting with Pro… (7 messages, latest: May 10 2020 at 13:27)
• Paper: Learning to Prove Theorems via Interacting with Proof (8 messages, latest: May 09 2020 at 23:55)
• Paper: Tactic Learning and Proving for the Coq Proof Assista (21 messages, latest: May 09 2020 at 23:51)
• Paper: Simple Dataset for … Isabelle/HOL (14 messages, latest: May 06 2020 at 23:54)
• Paper: Property Preserving Embedding of First-order Logic (3 messages, latest: May 04 2020 at 03:49)
• Paper: Prolog Technology Reinforcement Learning Prover (5 messages, latest: Apr 28 2020 at 23:43)
• Paper: Stateful Premise Selection by RNNs (2 messages, latest: Apr 28 2020 at 23:32)
• Paper: An Experimental Study of Formula Embeddings for Autom (18 messages, latest: Feb 09 2020 at 18:55)
• Proposal: Apply premise selection to Hammer (9 messages, latest: Jan 14 2020 at 03:41)
• Welcome! (10 messages, latest: Jan 14 2020 at 01:21)
• NEVER MIND. USE THIS STREAM NOW. (1 message, latest: Jan 14 2020 at 00:42)

---

Last updated: Dec 20 2025 at 21:32 UTC