Ecosyste.ms: Repos

An open API service providing repository metadata for many open source software ecosystems.

GitHub topics: formal-proofs

Repositories

Hacker-Code-J/Cryptol-CraftCodeLab

Mastering the Art of Cryptol Programming

Language: C - Size: 2.76 MB - Last synced: 6 days ago - Pushed: 6 days ago - Stars: 1 - Forks: 0

LogicalAtomist/principia

The Principia Rewrite

Language: TeX - Size: 10.2 MB - Last synced: 8 days ago - Pushed: 8 days ago - Stars: 199 - Forks: 5

pitmonticone/FLT Fork of ImperialCollegeLondon/FLT

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

Language: TeX - Size: 29.8 MB - Last synced: 8 days ago - Pushed: 8 days ago - Stars: 1 - Forks: 1

mo271/formal_book

Formalizing "Proofs from THE BOOK"

Language: Lean - Size: 229 KB - Last synced: 11 days ago - Pushed: 12 days ago - Stars: 35 - Forks: 6

xamidi/pmGenerator

An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.

Language: C++ - Size: 42.9 MB - Last synced: 17 days ago - Pushed: 17 days ago - Stars: 9 - Forks: 2

pthariensflame/agda-fumulas

An exploration of fumulas in Agda—a new perspective on ring theory

Language: Agda - Size: 92.8 KB - Last synced: 21 days ago - Pushed: 21 days ago - Stars: 1 - Forks: 0

SKolodynski/IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.

Language: Isabelle - Size: 110 MB - Last synced: 24 days ago - Pushed: 24 days ago - Stars: 16 - Forks: 2

pitmonticone/FLT3 Fork of riccardobrasca/flt3

A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.

Language: TeX - Size: 550 KB - Last synced: 25 days ago - Pushed: 25 days ago - Stars: 1 - Forks: 1

aripiprazole/rinha

🧪 | Rinha de Backend Lean4

Language: Lean - Size: 11.4 MB - Last synced: 6 days ago - Pushed: 9 months ago - Stars: 59 - Forks: 3

leanprover-community/mathlib

Lean 3's obsolete mathematical components library: please use mathlib4

Language: Lean - Size: 213 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 1,632 - Forks: 294

appliedfm/vstyle

A style guide for Coq

Size: 646 KB - Last synced: about 1 month ago - Pushed: over 2 years ago - Stars: 15 - Forks: 0

SergioBonatto/sergiobonatto.github.io

Meu site pessoal e blog onde posto coisas que acho interessantes

Language: HTML - Size: 2.67 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 0 - Forks: 0

coq-community/hydra-battles

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

Language: Coq - Size: 20.9 MB - Last synced: 24 days ago - Pushed: 3 months ago - Stars: 60 - Forks: 12

dtumad/lean-crypto-formalization

Library for formalizing cryptography proofs in Lean 3 (Deprecated)

Language: Lean - Size: 2.13 MB - Last synced: about 2 months ago - Pushed: about 2 months ago - Stars: 7 - Forks: 0

RiccardoBiosas/LeanGPT

Experiments with interactive theorem provers, LLMs and formal systems

Language: Coq - Size: 7.81 KB - Last synced: about 1 month ago - Pushed: 11 months ago - Stars: 12 - Forks: 2

Gastd/fptt

Solutions to Coq exercises from Formal proof: an Introduction to Type Theory class in 2018/1

Language: Coq - Size: 17.6 KB - Last synced: 2 months ago - Pushed: over 4 years ago - Stars: 0 - Forks: 0

unitb/temporal-logic

Language: Lean - Size: 254 KB - Last synced: 2 months ago - Pushed: over 5 years ago - Stars: 8 - Forks: 3

Matafou/LibHyps

A Coq library providing tactics to deal with hypothesis

Language: Coq - Size: 165 KB - Last synced: 24 days ago - Pushed: 5 months ago - Stars: 19 - Forks: 3

niltok/magic-in-ten-mins

十分钟魔法练习

Language: HTML - Size: 31.5 MB - Last synced: 3 months ago - Pushed: 9 months ago - Stars: 719 - Forks: 34

statebox/idris-ct

formally verified category theory library

Language: Idris - Size: 376 KB - Last synced: 3 months ago - Pushed: almost 4 years ago - Stars: 250 - Forks: 22

SyntakticSugar/kete

Small kete of mathematics formalized in Lean.

Language: Lean - Size: 21.5 KB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 0 - Forks: 0

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).

Language: ReScript - Size: 18 MB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 10 - Forks: 4

uben0/prove

A formal proof system in the terminal

Language: Rust - Size: 35.2 KB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 0 - Forks: 0

DanielBelchamber/DiscoveringTruth

Language: JavaScript - Size: 380 KB - Last synced: 5 months ago - Pushed: over 3 years ago - Stars: 0 - Forks: 0

atakeskinn/eudoxus-reals

An unusual construction of the real numbers using Isabelle/HOL

Language: Isabelle - Size: 814 KB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 0 - Forks: 0

atakeskinn/martingales

A Formalization of Martingales using Isabelle/HOL

Language: Isabelle - Size: 20 MB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 0 - Forks: 0

ecly/programming_language_seminar

Exercises and project for Programming Language Seminar course at ITU

Language: Coq - Size: 4.48 MB - Last synced: 6 months ago - Pushed: almost 6 years ago - Stars: 0 - Forks: 0

data61/PSL

Language: Isabelle - Size: 172 MB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 58 - Forks: 9

haztecaso/euclidean-geometry-lean

Trabajo de Fin de Grado de Matemáticas, en la Universidad Complutense de Madrid. Presentado en septiembre de 2023.

Language: TeX - Size: 40.4 MB - Last synced: 8 months ago - Pushed: 8 months ago - Stars: 0 - Forks: 0

Gbury/archsat

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

Language: OCaml - Size: 2.14 MB - Last synced: 6 months ago - Pushed: 11 months ago - Stars: 24 - Forks: 3

markpock/fitch-proof-for-propositional-logic

A utility for proofs in the propositional calculus. Currently finished - a way of parsing (most) valid strings in the PC as Sentences which can be added to proofs. Working on a mechanism for machine proof.

Language: Python - Size: 59.6 KB - Last synced: 10 months ago - Pushed: over 1 year ago - Stars: 2 - Forks: 1