From 54c1b82f8ec9907af66c3e95271d854df744d3a9 Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Mon, 23 Jun 2025 14:01:37 -0600 Subject: [PATCH] Fix #8 --- tools/sat-smt/lean.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 tools/sat-smt/lean.md diff --git a/tools/sat-smt/lean.md b/tools/sat-smt/lean.md new file mode 100644 index 0000000..1373863 --- /dev/null +++ b/tools/sat-smt/lean.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'LEAN' +subtitle = 'Programming Language & Theorem Prover' +links = [ + { title = "Homepage", url = "https://lean-lang.org/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/leanprover/lean4", icon = 'fa-brands fa-github' }, + # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' } +] +applications = ['Theorem Prover', 'Modeling Language'] +developers = ['Lean FRO'] +licenses = ['Apache-2.0'] +# inputs = ['SMTLIB2'] +# interfaces = ['CLI', 'Online'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['Barbosa2022'] ++++ + + +cvc5 is an automatic theorem prover for SMT problems. \ No newline at end of file