Alternatives and similar repositories for FormalML

Users that are interested in FormalML are comparing it to the libraries listed below

• leanprover / SampCert
  SampCert : Verified Differential Privacy
  ☆82Updated 6 months ago
• siddhartha-gadgil / lean-loris
  Experiments with some ways of automating reasoning in lean 4
  ☆17Updated last year
• eprover / PyRes
  Pedagogical first-order prover in Python
  ☆77Updated 5 months ago
• LASER-UMASS / TacTok
  The TacTok automated Coq proof script synthesis tool
  ☆17Updated last year
• uds-psl / coq-library-undecidability
  A library of mechanised undecidability proofs in the Coq proof assistant.
  ☆125Updated this week
• rocq-community / rocq-lean-import
  ☆24Updated last month
• ejgallego / pycoq
  Python bindings for the Coq interactive proof assistant
  ☆56Updated 3 years ago
• jtristan / stump-learnable
  ☆16Updated 4 years ago
• ccodel / verified-encodings
  Verifying encodings into propositional logic in Lean
  ☆12Updated 2 years ago
• avigad / lamr
  Logic and Mechanized Reasoning
  ☆109Updated 3 weeks ago
• tlringer / ml-for-proofs
  An open bibliography of machine learning for formal proof papers
  ☆32Updated 2 years ago
• data61 / PSL
  ☆73Updated last week
• logsem / clutch
  Probabilistic separation logics for verifying higher-order probabilistic programs.
  ☆27Updated this week
• JamesGallicchio / LeanColls
  WIP collections library for Lean 4
  ☆32Updated 6 months ago
• BartoszPiotrowski / lean-premise-selection
  ☆22Updated last year
• coq-tactician / coq-tactician
  A Seamless, Interactive Tactic Learner and Prover for Coq
  ☆78Updated last week
• verse-lab / splean
  Separation Logic Proofs in Lean
  ☆45Updated 7 months ago
• LS-Lab / KeYmaeraX-release
  KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
  ☆84Updated 4 months ago
• dwrensha / lean4-maze
  maze game encoded in Lean 4 syntax
  ☆65Updated 4 months ago
• siddhartha-gadgil / Saturn
  Experiments with SAT solvers with proofs in Lean 4
  ☆62Updated last year
• sneeuwballen / zipperposition
  An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logt…
  ☆151Updated last year
• agrarpan / coq-synthesis
  coq-synthesis is a Coq plugin for proof generation and next tactic prediction
  ☆13Updated last year
• siddhartha-gadgil / LeanAide
  Tools based on AI for helping with Lean 4
  ☆102Updated last week
• UCSD-PL / proverbot9001
  ☆43Updated 3 months ago
• bzhan / holpy
  Implementation of higher-order logic in Python
  ☆65Updated 2 years ago
• jtassarotti / coq-proba
  A Probability Theory Library for the Coq Theorem Prover
  ☆54Updated 2 years ago
• PatrickMassot / lean-verbose
  Very controlled natural language tactics for Lean
  ☆64Updated last year
• verse-lab / lean-ssr
  LeanSSR: an SSReflect-Like Tactic Language for Lean
  ☆39Updated 3 weeks ago
• leanprover-community / lftcm2020
  Lean for the Curious Mathematician 2020
  ☆68Updated 2 years ago
• paulaneeley / modal
  ☆16Updated 4 years ago