José A. Alonso · @Jose_A_Alonso
874 followers · 1892 posts · Server mathstodon.xyz
FIMO: A challenge formal dataset for automated theorem proving. ~ Chengwu Liu et als. https://arxiv.org/abs/2309.04295 #ITP #LeanProver #Math
José A. Alonso · @Jose_A_Alonso
868 followers · 1881 posts · Server mathstodon.xyzStudy of a division-like property. ~ Robin Khanfir, Béranger Seguin (@Moinsdeuxcat). https://arxiv.org/abs/2210.13078 #ITP #LeanProver #Math
José A. Alonso · @Jose_A_Alonso
864 followers · 1857 posts · Server mathstodon.xyzCan LLMs generate mathematical proofs that can be rigorously checked? Meet LeanDojo: An open-source AI playground with toolkits, benchmarks, and models for large language models to prove formal theorems in the Lean proof assistant. ~ Tanya Malhotra. https://www.marktechpost.com/2023/07/01/can-llms-generate-mathematical-proofs-that-can-be-rigorously-checked-meet-leandojo-an-open-source-ai-playground-with-toolkits-benchmarks-and-models-for-large-language-models-to-prove-formal-theore/ #AI #LLMs #ITP #LeanProver
José A. Alonso · @Jose_A_Alonso
859 followers · 1827 posts · Server mathstodon.xyzScaling Lean to the next millions of lines of proofs. ~ Sebastian Ullrich (@kha). https://leanprover.github.io/talks/WITS2023.pdf #ITP #LeanProver
José A. Alonso · @Jose_A_Alonso
853 followers · 1808 posts · Server mathstodon.xyzLoogle: a search tool for Lean/Mathlib. https://loogle.lean-fro.org #ITP #LeanProver #Mathlib
José A. Alonso · @Jose_A_Alonso
853 followers · 1806 posts · Server mathstodon.xyzMy experience at the Machine-Checked Mathematics workshop. ~ Jana Göken. https://bit.ly/3sknl6j #ITP #LeanProver #Math
awalterschulze · @awalterschulze
40 followers · 73 posts · Server fosstodon.org
#LeanProver is not just for proving programs are correct, but also great for writing imperative programs.
We tested it out with this LeetCode problem on Thursday, see more here: https://github.com/paulcadman/lean4-leetcode
José A. Alonso · @Jose_A_Alonso
848 followers · 1788 posts · Server mathstodon.xyzThe hitchhiker’s guide to logical verification (2023 standard edition). ~ Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, Jannis Limperg. https://raw.githubusercontent.com/blanchette/logical_verification_2023/main/hitchhikers_guide.pdf #eBook #ITP #LeanProver
José A. Alonso · @Jose_A_Alonso
845 followers · 1737 posts · Server mathstodon.xyz
Will machines eat mathematics? ~ Kevin Buzzard (@xenaproject). https://youtu.be/WNeS4J62v6g #ITP #LeanProver #Math
José A. Alonso · @Jose_A_Alonso
836 followers · 1710 posts · Server mathstodon.xyzAn extensible theorem proving frontend. ~ Sebastian Andreas Ullrich. https://publikationen.bibliothek.kit.edu/1000161074/151088087 #ITP #LeanProver
Anand Rao · @art
22 followers · 101 posts · Server mathstodon.xyz
#LeanSlides - a tool to automatically generate and render #revealjs slides from #markdown comments in the #lean editor: https://github.com/0art0/lean-slides/
#Lean4 #leanprover #lean #markdown #revealjs #leanslides
José A. Alonso · @Jose_A_Alonso
823 followers · 1662 posts · Server mathstodon.xyzFormally correct deduction methods for computational logic. ~ Asta Halkjær From. https://backend.orbit.dtu.dk/ws/portalfiles/portal/330349164/Afhandling_Asta_From.pdf #ITP #IsabelleHOL #LeanProver #Logic
#logic #leanprover #IsabelleHOL #itp
José A. Alonso · @Jose_A_Alonso
821 followers · 1648 posts · Server mathstodon.xyzProductivity tools for solver-aided programming. ~ Sorawee Porncharoenwase. https://www.proquest.com/openview/78dfe9e41f0f293c2e928713153c591e #ITP #LeanProver.
awalterschulze · @awalterschulze
39 followers · 70 posts · Server fosstodon.org
A Cheat Sheet for #Coq Proof Assistant users who are interested in #LeanProver
The repo includes an A4 pdf that you can print out and put on your wall for easy reference
José A. Alonso · @Jose_A_Alonso
820 followers · 1640 posts · Server mathstodon.xyzTowards a mathematics formalisation assistant using Large Language Models. ~ Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, Anand Tadipatri. https://arxiv.org/abs/2211.07524 #AI #LLMs #ITP #LeanProver #Math #Autoformalization
#autoformalization #math #leanprover #itp #LLMs #ai
José A. Alonso · @Jose_A_Alonso
813 followers · 1631 posts · Server mathstodon.xyzHow to explain advanced mathematics to a computer. ~ Riccardo Brasca. https://webusers.imj-prg.fr/~riccardo.brasca/event/luxembourg-2021/pres.pdf #ITP #LeanProver #Math
José A. Alonso · @Jose_A_Alonso
813 followers · 1631 posts · Server mathstodon.xyzWhat does it mean to formalise and why do it. ~ Riccardo Brasca. https://webusers.imj-prg.fr/~riccardo.brasca/event/rome-2023/rome.pdf #ITP #LeanProver #Math
José A. Alonso · @Jose_A_Alonso
811 followers · 1622 posts · Server mathstodon.xyzFermat’s last theorem for regular primes. ~ Alex J. Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi. https://drops.dagstuhl.de/opus/volltexte/2023/18374/pdf/lipics-vol268-itp2023-complete.pdf#page=637 #ITP #LeanProver #Math
José A. Alonso · @Jose_A_Alonso
811 followers · 1622 posts · Server mathstodon.xyzFormalising the Proj construction in Lean. ~ Jujian Zhang. https://drops.dagstuhl.de/opus/volltexte/2023/18374/pdf/lipics-vol268-itp2023-complete.pdf#page=619 #ITP #LeanProver #Math
José A. Alonso · @Jose_A_Alonso
811 followers · 1610 posts · Server mathstodon.xyzGroup cohomology in the Lean community library. ~ Amelia Livingston. https://drops.dagstuhl.de/opus/volltexte/2023/18374/pdf/lipics-vol268-itp2023-complete.pdf#page=377 #ITP #LeanProver #Math