Isabelle is described as 'Proof assistant for writing and checking mathematical proofs by computer' and is an app in the education & reference category. There are four alternatives to Isabelle for Mac, Windows, Linux, Web-based and Visual Studio Code. The best Isabelle alternative is Lean Prover, which is both free and Open Source. Other great apps like Isabelle are F*, Rocq Prover and Agda.
Lean is a functional programming language and interactive theorem prover based on dependent type theory. Dependent type theory unites the worlds of programs and proofs; thus, Lean is also a programming language.
Lean Prover is the most popular Windows, Mac & Linux alternative to Isabelle.
Lean Prover is the most popular Open Source & free alternative to Isabelle.
F* is an ML-like functional programming language aimed at program verification. F* can express precise specifications for programs, including functional correctness properties. Programs written in F* can be translated to OCaml or F# for execution.
F* is the most popular Web-based alternative to Isabelle.
A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more.
Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs...
United States
France
EU