Tags : Browse Projects

Select a tag to browse associated projects and drill deeper into the tag cloud.

Coq proof assistant

Analyzed about 16 hours ago

Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows: * to define functions or predicates, * to state mathematical theorems and software specifications, * to develop interactively formal proofs of these theorems, * to ... [More]

341K lines of code

74 current contributors

1 day since last commit

20 users on Open Hub

Very High Activity

I Use This

Mostly written in OCaml

Tags coq extraction functional functional_language language logic mathematics programming proof-assistant proof_assistant proving theorem 1 more...

Isabelle

No analysis available

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle is developed at University of Cambridge (Larry Paulson) and Technical University of Munich (Tobias Nipkow).

0 lines of code

17 current contributors

0 since last commit

2 users on Open Hub

Activity Not Available

I Use This

Mostly written in language not available

Licenses: BSD-3-Clause

Tags logic math proof proof_assistant

Skeptik

Analyzed about 12 hours ago

Proof theory and automated deduction framework focused on proof compression techniques and implemented in Scala.

15.2K lines of code

0 current contributors

over 9 years since last commit

1 users on Open Hub

Inactive

I Use This

Mostly written in Scala

Licenses: Creative_...

Tags logic proof_assistant proof_checker proofs proof_theory prooftheory proving scala theoremprover

software-foundations

S

Analyzed about 6 hours ago

Software Foundations in Idris

615 lines of code

1 current contributors

almost 7 years since last commit

0 users on Open Hub

Inactive

I Use This

Mostly written in Nix

Licenses: No declared licenses

Tags coq idris proof_assistant proofs textbook

lean

L

Analyzed about 2 hours ago

Lean Theorem Prover

4.58M lines of code

6 current contributors

about 7 hours since last commit

0 users on Open Hub

Very High Activity

I Use This

Mostly written in C

Licenses: apache_2

Tags proof_assistant proofassistant prooftheory theoremprover

rzk

R

Analyzed about 11 hours ago

An experimental proof assistant based on a type theory for synthetic ∞-categories.

9.75K lines of code

0 current contributors

22 days since last commit

0 users on Open Hub

Low Activity

I Use This

Mostly written in Haskell

Licenses: No declared licenses

Tags proof-assistant proof_assistant

holbert

H

Analyzed about 11 hours ago

A graphical interactive proof assistant designed for education

4.24K lines of code

0 current contributors

10 months since last commit

0 users on Open Hub

Very Low Activity

I Use This

Mostly written in Haskell

Licenses: No declared licenses

Tags proof_assistant