Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topics:

Cap set improvement (2 messages, latest: Dec 20 2023 at 08:49)
LeanGPT (11 messages, latest: Dec 20 2023 at 05:01)
MATH-AI workshop at NeurIPS (51 messages, latest: Dec 19 2023 at 18:15)
ML for Theorem Proving Tutorial - NeurIPS 2023 (89 messages, latest: Dec 19 2023 at 05:13)
LeanCopilot (67 messages, latest: Dec 19 2023 at 03:35)
COPRA (69 messages, latest: Dec 19 2023 at 01:24)
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)
Lean Chat is publicly available (30 messages, latest: Dec 04 2023 at 12:58)
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)
Testimonials (2 messages, latest: Sep 15 2023 at 12:25)
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)
Releasing LeanDojo (65 messages, latest: Aug 23 2023 at 18:49)
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)
New paper: Magnushammer (23 messages, latest: Apr 19 2023 at 00:47)
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 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)
dreamcoder (32 messages, latest: Apr 22 2021 at 21:48)
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 2023 at 11:08 UTC