Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topics:

VibeRegistry / slopnet (5 messages, latest: Feb 27 2026 at 18:03)
Diamond problems and universes (1 message, latest: Feb 26 2026 at 17:31)
AlphaProof Paper (discussion) (20 messages, latest: Feb 26 2026 at 03:50)
Aristotle Partial Results (2 messages, latest: Feb 24 2026 at 18:22)
Aristotle and axioms (13 messages, latest: Feb 24 2026 at 15:29)
chatgpt proved a theorem in 6 minutes and 20 seconds (3 messages, latest: Feb 24 2026 at 01:23)
OpenCode (18 messages, latest: Feb 23 2026 at 21:14)
PutnamBench (85 messages, latest: Feb 23 2026 at 06:38)
Opus 4.6 is great at formal proofs (Rocq/Lean4) (44 messages, latest: Feb 22 2026 at 15:10)
Theorem Search (5 messages, latest: Feb 21 2026 at 23:03)
APRIL: a dataset for learning error correction (3 messages, latest: Feb 21 2026 at 07:31)
Learning to golf with Aristotle. (9 messages, latest: Feb 20 2026 at 04:06)
zero-trust AI benchmark (12 messages, latest: Feb 19 2026 at 17:49)
great 8b models for generating lean proofs? (11 messages, latest: Feb 18 2026 at 17:25)
Sonnet 4.6 (1 message, latest: Feb 18 2026 at 12:19)
MerLean: autoformalization in quantum computation (13 messages, latest: Feb 15 2026 at 09:43)
OpenAI Result in Theoretical Physics (5 messages, latest: Feb 14 2026 at 13:19)
DeepMind's Aletheia Erdos problem (11 messages, latest: Feb 12 2026 at 17:02)
packaging Lean in apt for Claude? (18 messages, latest: Feb 10 2026 at 16:47)
Theorem Proving for Machine Learning (9 messages, latest: Feb 09 2026 at 12:54)
AxiomProver solves an open problem (31 messages, latest: Feb 07 2026 at 17:16)
Numina-Lean-Agent solves 12 problems on Putnam2025 (14 messages, latest: Feb 05 2026 at 04:15)
Discussion: Posts on AI, Lean, Mathematics (14 messages, latest: Jan 30 2026 at 18:48)
Lean Skill for Claude Code (34 messages, latest: Jan 30 2026 at 15:37)
Anthropic in IMO/Putnam/PutnamBench/Erdos ? (16 messages, latest: Jan 29 2026 at 23:18)
Understanding what Aristotle is formalizing (6 messages, latest: Jan 29 2026 at 23:09)
TheoremForge: Agentic Workflow for Data Synthesis (7 messages, latest: Jan 29 2026 at 08:12)
Neural Theorem Proving for Verification Conditions (1 message, latest: Jan 28 2026 at 16:03)
Aristotle's waitlist is gone (32 messages, latest: Jan 26 2026 at 23:33)
Autotranslation of Logical Foundations from Rocq to Lean (5 messages, latest: Jan 18 2026 at 13:27)
LeanCat benchmark (category theory in Lean 4) (30 messages, latest: Jan 16 2026 at 10:11)
A (semi)-autoformalization challenge: 650=>448 (27 messages, latest: Jan 15 2026 at 21:22)
Discussion: How will autoproving impact math? (13 messages, latest: Jan 15 2026 at 18:54)
Autoformalization using Megalodon (10 messages, latest: Jan 15 2026 at 09:18)
AxiomProver solves Putnam 2025 (4 messages, latest: Jan 11 2026 at 02:42)
Claude Code Aristotle Plugin (1 message, latest: Jan 10 2026 at 11:09)
✔ Lean Zulip Chat Dataset (66 messages, latest: Dec 29 2025 at 13:43)
Prove linear algebra by Aristotle (21 messages, latest: Dec 28 2025 at 18:22)
ashme/aime in lean in < 10GB weights ? (10 messages, latest: Dec 25 2025 at 21:53)
Seed Prover 1.5 proves 11 / 12 Putnam 2025 in 9 hours (23 messages, latest: Dec 25 2025 at 07:13)
AI-discovered proof on psi-integrals (with Lean formalizat.) (34 messages, latest: Dec 20 2025 at 12:48)
Discussion of Gödel's Poetry: Open source, recursive prover (1 message, latest: Dec 17 2025 at 16:34)
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)
Discussion: Goedel-Prover-V2: A new SOTA model (51 messages, latest: Dec 10 2025 at 12:59)
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)
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)
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)
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)
✔ 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: Feb 28 2026 at 14:05 UTC