Topic: lean4 Goto Github

👇 Here are 316 public repositories matching this topic...

34j / best-of-lean4
lean4,A list of awesome lean4 projects. Feel free to add your project.
User: 34j
awesome best-of lean lean4

aripiprazole / rinha
lean4,🧪 | Rinha de Backend Lean4
User: aripiprazole
Home Page: https://meoowers.github.io/rinha/rinhabackendsimulation-20230911191507033/
formal-proofs lean4 pgsql rinha-de-backend-2023-q3

dwrensha / compfiles
lean4,Catalog Of Math Problems Formalized In Lean
User: dwrensha
Home Page: https://dwrensha.github.io/compfiles/
lean4

dwrensha / lean4-maze
lean4,maze game encoded in Lean 4 syntax
User: dwrensha
Home Page: https://live.lean-lang.org/#url=https%3A%2F%2Fraw.githubusercontent.com%2Fdwrensha%2Flean4-maze%2Fmain%2FMaze.lean
lean4

eric-wieser / lean-matrix-cookbook
lean4,The matrix cookbook, proved in the Lean theorem prover
User: eric-wieser
lean matrices formal-mathematics lean4

forked-from-1kasper / ground_zero
lean4,Ground Zero: Lean 4 HoTT Library
User: forked-from-1kasper
math cubical-type-theory ctt homotopy-type-theory hott lean leanprover lean4

formalizedformallogic / foundation
lean4,Lean4 Logic Formalization
Organization: formalizedformallogic
Home Page: https://formalizedformallogic.github.io/Book/
lean4 logic incompleteness

galoisinc / lean4-balance-car
lean4,Lean4 port of Arduino balance car controller
Organization: galoisinc
lean4

google-deepmind / debate
lean4,Formalizing stochastic doubly-efficient debate
Organization: google-deepmind
lean4

hrmacbeth / math2001
lean4,Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant
User: hrmacbeth
lean4

ipdsnelting / tba-2021
lean4,Materials for the course "theorem prover lab: applications in programming languages" at KIT, SS2021 edition
Organization: ipdsnelting
Home Page: https://pp.ipd.kit.edu/lehre/SS2021/tba/
lean4

joehendrix / lean-crypto
lean4,Cryptographic routines for the Lean 4 language
User: joehendrix
lean4

julian / lean.nvim
lean4,neovim support for the Lean theorem prover
User: julian
leanprover neovim neovim-plugin lean nvim-treesitter tree-sitter nvim lean4

kmill / lean4-raytracer
lean4,A simple raytracer written in Lean 4
User: kmill
lean4 raytracing

lean-dojo / leancopilot
lean4,LLMs as Copilots for Theorem Proving in Lean
Organization: lean-dojo
Home Page: https://leandojo.org
lean llm-inference machine-learning theorem-proving lean4 formal-mathematics

lean-dojo / leandojo
lean4,Tool for data extraction and interacting with Lean programmatically.
Organization: lean-dojo
Home Page: https://leandojo.org
lean lean4 machine-learning theorem-proving

leanprover-community / aesop
lean4,White-box automation for Lean 4
Organization: leanprover-community
lean4

leanprover-community / batteries
lean4,The "batteries included" extended library for the Lean programming language and theorem prover
Organization: leanprover-community
lean4 lean

leanprover-community / con-nf
lean4,A formal consistency proof of Quine's set theory New Foundations
Organization: leanprover-community
Home Page: https://leanprover-community.github.io/con-nf/
lean4 set-theory new-foundations

leanprover-community / duper
lean4,
Organization: leanprover-community
lean4

leanprover-community / lean4-metaprogramming-book
lean4,
Organization: leanprover-community
Home Page: https://leanprover-community.github.io/lean4-metaprogramming-book/
lean4

leanprover-community / lean4-mode
lean4,Emacs major mode for Lean 4
Organization: leanprover-community
Home Page: https://leanprover.github.io/
emacs lean4

leanprover-community / lean4-samples
lean4,Code samples for Lean 4
Organization: leanprover-community
lean4

leanprover-community / lean4game
lean4,Server to host lean games.
Organization: leanprover-community
Home Page: https://adam.math.hhu.de
lean4 react

leanprover-community / lean4web
lean4,The Lean 4 web editor
Organization: leanprover-community
Home Page: https://live.lean-lang.org/
lean4

leanprover-community / mathlib4
lean4,The math library of Lean 4
Organization: leanprover-community
Home Page: https://leanprover-community.github.io/mathlib4_docs
lean4

leanprover-community / nng4
lean4,Natural Number Game
Organization: leanprover-community
Home Page: https://adam.math.hhu.de
lean4

leanprover-community / proofwidgets4
lean4,Helper toolkit for creating your own Lean 4 UserWidgets
Organization: leanprover-community
lean lean4 visualization

leanprover-community / quote4
lean4,Intuitive, type-safe expression quotations for Lean 4.
Organization: leanprover-community
lean4

leanprover / doc-gen4
lean4,Document Generator for Lean 4
Organization: leanprover
lean4

leanprover / lake
lean4,**(Deprecated: Merged into Lean 4)** Lean 4 build system and package manager with configuration files written in Lean.
Organization: leanprover
lean4

leanprover / lean4
lean4,Lean 4 programming language and theorem prover
Organization: leanprover
Home Page: https://lean-lang.org
lean4 lean

leanprover / lean4-cli
lean4,A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.
Organization: leanprover
cli lean lean4

leanprover / leanink
lean4,LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Organization: leanprover
lean4 alectryon visualization lean interactive-theorem-proving

leanprover / lnsym
lean4,Armv8 Native Code Symbolic Simulator in Lean
Organization: leanprover
lean4

leanprover / theorem_proving_in_lean4
lean4,Theorem Proving in Lean 4
Organization: leanprover
Home Page: https://leanprover.github.io/theorem_proving_in_lean4/
lean4 lean

lecopivo / scilean
lean4,Scientific computing in Lean 4
User: lecopivo
lean4 scientific-computing numerical-methods symbolic-computation

loganrjmurphy / leaneuclid
lean4,LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
User: loganrjmurphy
Home Page: http://arxiv.org/abs/2405.17216
autoformalization euclidean-geometry formalization lean4 llm-evaluation theorem-proving

nomeata / loogle
lean4,Mathlib search tool
User: nomeata
Home Page: https://loogle.lean-lang.org/
lean4 lean

opencompl / lean-mlir-old
lean4,embedding MLIR in LEAN
Organization: opencompl
compilers lean4 llvm mlir

paper-proof / paperproof
lean4,Lean theorem proving interface which feels like pen-and-paper proofs.
Organization: paper-proof
lean4 mathematics proof-tree

patrickmassot / verbose-lean4
lean4,Natural language tactics to teach mathematics using Lean 4
User: patrickmassot
lean4 mathematics-education

rami3l / plfl
lean4,Learn Lean 4 with PLFA proofs.
User: rami3l
lean lean4 plfa programming-language-foundations software-foundations

risc0 / risc0-lean4
lean4,A model of the RISC Zero zkVM and ecosystem in the Lean 4 Theorem Prover
Organization: risc0
lean lean4 risc0 zero-knowledge zk-stark zkvm risc-v riscv riscv32 riscv32im

siddhartha-gadgil / leanaide
lean4,Tools based on AI for helping with Lean 4
User: siddhartha-gadgil
lean4

siddhartha-gadgil / saturn
lean4,Experiments with SAT solvers with proofs in Lean 4
User: siddhartha-gadgil
lean4

tydeu / lean4-alloy
lean4,Write C shims from within Lean code.
User: tydeu
lean4

ufmg-smite / lean-smt
lean4,Tactics for discharging Lean goals into SMT solvers.
Organization: ufmg-smite
lean4 smt

verified-optimization / cvxlean
lean4,Convex optimization modeling in Lean 4
Organization: verified-optimization
convex-optimization lean4 formal-verification interactive-theorem-proving

wellecks / llmstep
lean4,llmstep: [L]LM proofstep suggestions in Lean 4.
User: wellecks
lean lean4 llm theorem-proving