Aristotle API
The World's Most Advanced Formal Reasoning Agent> Get access nowWhat others are saying about Aristotle... We’re the #1 formal math model according to ProofBench, by @ValsAI, ahead of the closest competitor by 15%. Aristotle Agent can autonomously prove/formalize for up to 24 hrs without human intervention.
Loogle!
About Loogle searches Lean and Mathlib definitions and theorems. You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot. Usage Loogle finds definitions and lemmas in various ways: By constant: 🔍 Real.sin
Functional Programming in Lean - Functional Programming in Lean
Functional Programming in Lean by David Thrane Christiansen Copyright Microsoft Corporation 2023 This is a free book on using Lean 4 as a programming language. All code samples are tested with Lean 4 release 4.1.0. Release history January, 2024 This is a minor bugfix release that fixes a regression in an example program. October, 2023 In this first maintenance release, a number of smaller issues w
Lean Programming Language
Functional Programming in Lean (FPIL) is the main resource for programmers who want to learn Lean. It assumes a background in programming, but no prior knowledge of functional programming is needed. Theorem Proving in Lean (TPIL) is designed to teach you to develop and verify proofs in Lean and covers dependent type theory, automated proof methods, and Lean-specific features for interactive theore
Theorem Proving in Lean 4
Jeremy AvigadLeonardo de MouraSoonho KongSebastian Ullrich with contributions from the Lean Community This version of the text assumes you’re using Lean 4 (specifically 4.26.0). See the Quickstart section of the Lean documentation to install Lean. The first version of this book was written for Lean 2, and the Lean 3 version is available here.
Theorem Proving in Lean 4 日本語訳 - Theorem Proving in Lean 4 日本語訳
Theorem Proving in Lean 4 by Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, with contributions from the Lean Community このテキストは読者がLean 4を使うことを前提にしています。Lean 4をインストールするには、Lean 4 Manualの節Quickstartをご覧ください。このテキストの最初のバージョンはLean 2用に書かれました。Lean 3用のバージョンはこちらで入手可能です。 この翻訳について translated by aconite(2章～12章), Haruhisa Enomoto(1章) この翻訳は有志による非公式翻訳です。翻訳に際して、表現を大きく変えた箇所や、分かりやすさを期すため記述やコード例を追加
A Formal Verification of Rust's Binary Search Implementation
This post is about my ongoing master’s thesis under Jeremy Avigad at Carnegie Mellon University, in which I’m trying to tackle formal verification of Rust programs in the interactive theorem prover Lean, and a first result of the project: a complete verification of the Rust stdlib’s binary search function. Putting the ‘Formal’ into ‘Formaldehyde’ Formal Verification is the act of mathematically re
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - lean-dojo/LeanCopilot: LLMs as Copilots for Theorem Proving in Lean
Moogle: Semantic search over mathlib4
Learning Lean 4
GitHub - leanprover-community/mathlib4: The math library of Lean 4
GitHub - Kha/electrolysis: Simple verification of Rust programs via functional purification in Lean 2(!)
GitHub - leanprover/theorem_proving_in_lean: Theorem proving in Lean
Lean Web Editor