brillant idea

work you guys put in Cedar is amazing🤟.. its hard problem to solve as this is tied to data modeling and you cant offload to vendors! from what i hear in 14:38 and 58:20 , application or applications have to provide a map of groups even though there is multiple levels of hierarchy to make the policy check quick. this is a data integration problem where loads of vendors are already competing!!

here's the same code but for Lean4: import Mathlib.Tactic.Linarith import Mathlib.Tactic import Mathlib open Nat theorem infinite_primes : ∀ N : ℕ ,∃ p ≥ N , Nat.Prime p := by intro N let M := N.factorial + 1 let p := Nat.minFac M have h0 : Nat.Prime p := by refine minFac_prime ?n1 have : N.factorial > 0 := by exact factorial_pos N linarith use p apply And.intro { by_contra h have h1 : p ∣ Nat.factorial N + 1 := by exact minFac_dvd M have h2 : p ∣ Nat.factorial N := by refine h0.dvd_factorial.mpr ?_ exact Nat.le_of_not_ge h have h3 : p ∣ 1 := (Nat.dvd_add_right h2).mp h1 exact Nat.Prime.not_dvd_one h0 h3 } { exact h0 }

what version of lean is this?

What's the Lean 4 equivalent of library_search?

Audio is definitely clipping. Come on guys.

4:51 my Lean interprets the exclamation mark as a "not" and I get type mismatch in that case.

Thank you for teaching me a really fun new way of validating mathematical proofs

Is there a place that shows all the theorems that Lean currently has?

Has this been able to prove any new results in mathematics?

Consider F = open nhds of x. Let's check it satisfies property 2. So let U be any nbhd of x. Then consider V to be a closed set that contains U. Then V is not in F. So the initial suggested filter is wrong. I assume I'm wrong so where is my mistake?

lean-slides is very cool

unknown identifier 'lemma' Lean (version 4.5.0, commit 1a3021f98e55, Release)

I remember reading about how prover 9 found a shorter version of the ontological argument. Which I thought was cool at the time. Of course I guess it is needless to say that did not really the settle the matter of the existence of god in any significant way. But I would be interested to see this method tackle that as well.

The start is missing context…

Between omega and verso, this has been a very exciting update!!

Brilliant!

Excellent work!

wonder if they detect license conflicts

seems neat but far too much content for the amount of time. its just not really comprehensible without more explanation per slide, and it's impossible to explain enough when you only spend like 10 seconds per slide.

using e-graphs, wow awesome!

Slides at leanprover.zulipchat.com/user_uploads/3121/YKeTqF-2-nn2UjoQcYjpRE5b/local_fields.pdf

If coq syntax allows it a better name may be Dec?

Cool stuff! I hope SciLean gets more support. I share Tomas's intuition that Lean is a very powerful language for scientific computing because of its ability to handle mathematics natively. We just need the software libraries like SciLean to fulfill that potential. Someone give him a bunch of money to work on this please.

I wonder if someone verified it's correctness

Slides for the talk: quatramaran.salle-s.org/~smorel/grassmannians.pdf Code: github.com/smorel394/ExteriorPowers

Slides are at leanprover.zulipchat.com/user_uploads/3121/7vc5TL4P0vSG_Je2fWW_sQEu/lean-together-2024.pdf

Hmm, isn't the functor from Top to Cond^light fully faithful on sequential spaces more generally? That was the impression I got from the current course on analytic stacks. The functor from Top to Cond was ff on compactly-generated spaces, iirc, certainly not all of them.

Slides are at slides.com/lecopivo/talk-at-nantes-493743

would be cool to formalize snarks from graph theory! (like nowhere-zero flows, or cycle double covers)

Thank you for your great presentation, Alex. I also feel that I wish I have the necessary information that I could foresee when I finish writing my thesis on Frege's Arithmetic.

The speakers assessment of Generative AI (e.g. chatgpt and other LLMs) is based on a 2016 paper? He badly misunderstands the area. Progress has been exponential since about 2019, and soon LLMs will be writing whole math papers in Lean and LaTeX. It wont be long before more than half the PRs in Mathlib are written primarily by LLMs, and Lean community needs to be ready for that. Edit: source, i work in AI and keep track of its use in mathematics. it's moving insanely fast. as soon as someone combines LLMs with MCTS and gives it a strong theorem checker like Lean to evaluate its guesses, it's going to make progress in math the same way AlphaGo made progress in Go. and I believe microsoft and google are both working on exactly that. so it wont be long now. anyone in math not tracking this closely is gonna be shocked, and may find their next paper's results scooped by an AI, or a human using an AI to help them prove theorems faster than any human can alone.

Lean is an incredible feat of engineering.

As part of docs: better error messages

from first pains / principles! :D brave demo

Does the lean file exist somewhere on the internet? I want to look at the exercises.

Hey gorgeous video: question if you have time: what is the difference between an axiomatic approach to geometry and say a non-axiomatic approach? Is linear algebra an axiomatic or non-axiomatic approach to geometry? If not what would be? Thanks!

Mathematicians are ephemeral people. Most of them will fade away into posh universities, obscure think tanks, and into government. The majority of new breakthroughs in mathematics will be made by corporations and individual engineers.

would be helpful if you could link the project repo in the description!

🎯 Key Takeaways for quick navigation: 00:01 🎙️ *Introduction to the talk and the speaker's background.* - The speaker, Kaiyu Yang, introduces himself and his work in using machine learning to improve theorem proving. - He outlines the purpose of his talk, which is to provide an overview of work in the domain of machine learning for theorem proving and its relevance to mathematicians. 02:15 🧮 *Automated theorem proving and its challenges.* - Explanation of automated theorem proving as the process of having computers find proofs automatically. - Discussion of the challenges in automated theorem proving, including the vast search space and the need for high-level mathematical intuition. 05:14 🤖 *Proof assistance in Lean and its role.* - Introduction to proof assistance tools like Lean, which involve human interaction with tactics to guide the proof process. - Highlighting the importance of human guidance in finding mathematical proofs. 08:18 📝 *Overview of large language models and their training.* - Explanation of large language models like GPT-4 as mappings between input and output strings. - Overview of pre-training and alignment steps in training large language models. 12:07 📋 *Different ways to use large language models.* - Discussion of two main ways to utilize large language models: prompting and fine-tuning. - Explanation of how large language models can be fine-tuned for specific tasks. 13:27 🤔 *The role of large language models in theorem proving.* - Introduction to the use of large language models for theorem proving. - Mention of other machine learning models for theorem proving. 15:49 🧩 *The idea of proof artifact code training.* - Explanation of proof artifact code training as a method to augment training data for large language models by adding auxiliary tasks. - Highlighting the improvement in performance achieved through this approach. 16:56 🧪 *The MiniF2F benchmark for theorem proving.* - Introduction to the MiniF2F dataset, focusing on mathematical Olympiad problems. - Discussion of the challenges in formalizing problems that require numerical answers and handling geometry. 18:40 🏫 *Curriculum learning for domain-specific theorem proving.* - Explanation of curriculum learning for domain-specific theorem proving, where the model iteratively improves on a new domain. - Presentation of results showing the effectiveness of this approach. 22:33 🧰 *OpenAI's efforts to support open-source research in theorem proving.* - Discussion of the barriers in open-source research in theorem proving. - Presentation of OpenAI's contributions, including tools, datasets, and open-source models, to facilitate research in the field. 26:20 📚 *Retrieval-augmented models for theorem proving.* - Introduction to retrieval-augmented models, addressing the issue of premise selection. - Explanation of how these models compile a list of relevant premises to assist in theorem proving. 27:16 📚 *Retrieval Augmented Prover* - The model retrieves relevant premises using cosine similarity between the proof state and premises. - Combines retrieved premises with the current proof state to generate tactics. 28:51 🤖 *GPT-4 and Lindo Demo* - Demonstrates GPT-4 interacting with Lindo to perform theorem proving. - Shows GPT-4 executing tactics and completing a proof. 31:24 🧩 *Auto Formalization in Ling* - Discusses the task of translating natural language theorems into formal versions. - Highlights challenges in evaluation due to formalization variations. 32:47 🤝 *Leveraging Informal Math Knowledge* - Explores how informal math knowledge can guide formal proof using proof sketches. - Describes a three-step process involving drafting, sketching, and proofing. 35:15 🚀 *Building Proof Automation Tools* - Discusses the need for proof automation tools for Lean users. - Highlights the differences in requirements between machine learning researchers and Lean users. Made with HARPA AI

I would like to see someone live-code an undergraduate exercise sheet. Just to see how easy or hard it is for someone knowledgeable to formalize trivial things. That would really showcase the API and demonstrate that it's usable.

Would be more enjoyable with less "ehm"

Quite interesting! It seems we lose the sound at 39:04 :(

Started easy enough. Sadly the sound cuts off at around 39 mina.

Cool!

This is exciting!

You could simply reject responses that change the signature.

😠 'promo sm'

Very useful and well made video ! Thank you for taking the time to make it

LOL these ae so stupid