Zulip Chat Archive
Stream: Machine Learning for Theorem Proving
Topics:
- DeepSeek-Prover V2 (154 messages, latest: May 02 2025 at 02:33)
- setting up leantool in roo-code (19 messages, latest: May 02 2025 at 02:10)
- 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)
- PutnamBench (80 messages, latest: May 01 2025 at 22:17)
- ✔ Lean Zulip Chat Dataset (65 messages, latest: May 01 2025 at 19:40)
- Hard proof-based auto-formalization benchmark (16 messages, latest: May 01 2025 at 13:12)
- Building up Lean.Expr's (10 messages, latest: May 01 2025 at 09:24)
- ✔ 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)
- request for help on the REPL (75 messages, latest: Apr 28 2025 at 15:20)
- 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)
- Kimina Lean Server (1 message, latest: Apr 24 2025 at 16:07)
- 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)
- Proof or Bluff (49 messages, latest: Apr 18 2025 at 10:31)
- 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)
- A proposal for Safe and Hallucinatio-free coding AI (27 messages, latest: Apr 14 2025 at 01:51)
- 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)
- Lean State Search: Search Mathlib theorems with proof states (17 messages, latest: Mar 10 2025 at 10:08)
- ✔ 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)
- Claude Code (7 messages, latest: Feb 26 2025 at 16:26)
- 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)
- Incentives & sorry-filling leaderboard (99 messages, latest: Feb 24 2025 at 20:29)
- 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)
- Autoformalisation (11 messages, latest: Aug 12 2024 at 08:23)
- $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)
- Releasing LeanDojo (68 messages, latest: Apr 22 2024 at 11:39)
- 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)
- (deleted) (1 message, latest: Mar 04 2023 at 18:13)
- 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
HyperTreepaper orEquations? (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: May 02 2025 at 03:31 UTC