GitHub topics: proof

Mk9207/-Constructive-Collatz-Conjecture

このリポジトリは、コラッツ予想に対する構成的完全証明を示します。あらゆる自然数が、特定の再帰的変換を経て最終的に1へと収束することを、合同類の構造論理とループ排除の形式によって証明します。 This repository presents a constructive complete proof of the Collatz Conjecture. It shows that any natural number ultimately converges to 1 via recursive transformation, using congruence class structure and loop elimination.

Size: 3.91 KB - Last synced at: about 23 hours ago - Pushed at: about 24 hours ago - Stars: 0 - Forks: 0

GasStationManager/CodeProofTheArena

Lean coding problem solving challenge website with proof verification

Language: Python - Size: 97.7 KB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 10 - Forks: 0

daviddoret/punctilious

A human-friendly and developer-friendly math proof assistant

Language: Python - Size: 55.1 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 2 - Forks: 0

xayahrainie4793/minimal-elements-of-the-prime-numbers

The minimal elements of the prime numbers which are > b written in the positional numeral system with radix b, as digit strings under the subsequence ordering, for 2 ≤ b ≤ 36

Language: C++ - Size: 172 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 1 - Forks: 0

eddieoz/haal

Hääl - Anonymous Electronic Voting System on Public Blockchains

Language: JavaScript - Size: 1.42 MB - Last synced at: 3 days ago - Pushed at: over 2 years ago - Stars: 115 - Forks: 17

msoos/cryptominisat

An advanced SAT solver

Language: C++ - Size: 58.8 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 865 - Forks: 195

seL4/website

The seL4.systems website

Language: HTML - Size: 421 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 3 - Forks: 13

creusot-rs/creusot

Creusot helps you prove your code is correct in an automated fashion.

Language: Rust - Size: 68.2 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 1,284 - Forks: 58

agda/agda-stdlib

The Agda standard library

Language: Agda - Size: 552 MB - Last synced at: 2 days ago - Pushed at: 5 days ago - Stars: 616 - Forks: 248

eyereasoner/eye-js

A distribution of EYE reasoner in the JavaScript ecosystem using Webassembly.

Language: TypeScript - Size: 489 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 50 - Forks: 5

scoredetect/timestamps

Timestamp your WordPress content into the blockchain to empower your content authenticity and increase user trust.

Language: PHP - Size: 2.14 MB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 2 - Forks: 0

lhitori/uxm

Unusable eXpression Manager

Language: OCaml - Size: 32.2 KB - Last synced at: 6 days ago - Pushed at: 9 days ago - Stars: 0 - Forks: 0

formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

Language: Rocq Prover - Size: 118 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 920 - Forks: 31

binary-translation/lasagne-proofs

Architecture mapping proofs written in Agda for the paper "Lasagne: A Static Binary Translator for Weak Memory Model Architectures"

Language: Agda - Size: 163 KB - Last synced at: 3 days ago - Pushed at: about 3 years ago - Stars: 14 - Forks: 2

michelleyogogirls/mocktail-generator

simple mocktail recipe generator

Language: JavaScript - Size: 5.86 KB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 0 - Forks: 0

mrieppel/FitchFX

Fitch proof constructor (using rules from my version of the forall x textbook)

Language: JavaScript - Size: 477 KB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 6 - Forks: 3

GuilhermeStracini/POC-dotnet-Dijkstra

🔬 Proof of Concept of Dijkstra's algorithm in .NET

Language: C# - Size: 501 KB - Last synced at: 4 days ago - Pushed at: 14 days ago - Stars: 3 - Forks: 0

jirilebl/ra

Basic Analysis, undergraduate real analysis textbook

Language: TeX - Size: 7.36 MB - Last synced at: 8 days ago - Pushed at: about 1 month ago - Stars: 76 - Forks: 26

OolonColoophid/bakerStreet

A natural deduction helper for macOS

Language: Swift - Size: 46.2 MB - Last synced at: 16 days ago - Pushed at: 16 days ago - Stars: 2 - Forks: 0

seL4/l4v

seL4 specification and proofs

Language: Isabelle - Size: 97.1 MB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 547 - Forks: 110

GuilhermeStracini/POC-react-dotnet-UploadStream

🔬 Proof of Concept of an upload stream from React (JS & Native) app to.NET

Language: JavaScript - Size: 3.25 MB - Last synced at: 19 days ago - Pushed at: 19 days ago - Stars: 1 - Forks: 0

gapt/gapt

GAPT: General Architecture for Proof Theory

Language: Scala - Size: 182 MB - Last synced at: 15 days ago - Pushed at: 15 days ago - Stars: 100 - Forks: 19

anarkrypto/P2PoW 📦

A P2P Delegated Proof of Work solution for Nano cryptocurrency

Language: JavaScript - Size: 11.1 MB - Last synced at: 5 days ago - Pushed at: about 2 years ago - Stars: 26 - Forks: 3

PrincetonUniversity/VST

Verified Software Toolchain

Language: Coq - Size: 74.9 MB - Last synced at: about 4 hours ago - Pushed at: about 5 hours ago - Stars: 463 - Forks: 94

orange-you-glad/spectral-proof-of-RH

A modular, CI-verified formal manuscript that constructs a canonical trace-class operator whose spectral determinant encodes the completed Riemann zeta function—culminating in a spectral equivalence formulation of the Riemann Hypothesis. Includes DAG-audited proofs, Lean compatibility scaffolds, and agent-safe modular structure.

Language: TeX - Size: 82.1 MB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 1 - Forks: 0

DigitalFormalLogic/mathesis

Python library for computational formal logic, formal semantics, and theorem proving

Language: Python - Size: 1.23 MB - Last synced at: 1 day ago - Pushed at: 30 days ago - Stars: 22 - Forks: 2

Splines/lean-continuous

Continuous functions formalized in Lean4. A students project accompanied by a YouTube video.

Language: TeX - Size: 5.44 MB - Last synced at: 9 days ago - Pushed at: 11 months ago - Stars: 15 - Forks: 2

LS-Lab/KeYmaeraX-projects

Projects, models, and proofs in KeYmaera X

Language: Shell - Size: 955 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 7 - Forks: 8

w3c/vc-di-bbs

A linked data proof suite specification for BBS+ signatures

Language: HTML - Size: 733 KB - Last synced at: about 1 month ago - Pushed at: 3 months ago - Stars: 51 - Forks: 21

AstraaDev/NitroProof-Gen

Generate an image (.png) simulating the donation of a nitro to a user

Language: Python - Size: 388 KB - Last synced at: about 1 month ago - Pushed at: 3 months ago - Stars: 82 - Forks: 48

xiaoshihou514/ndpc

Natural deduction proof compiler

Language: Scala - Size: 227 KB - Last synced at: about 22 hours ago - Pushed at: about 1 month ago - Stars: 8 - Forks: 0

xiaoshihou514/aristotle

Easy to use gui frontend for ndpc

Language: C++ - Size: 165 KB - Last synced at: about 22 hours ago - Pushed at: about 2 months ago - Stars: 2 - Forks: 0

uwplse/verdi

A framework for formally verifying distributed systems implementations in Coq

Language: Coq - Size: 2.55 MB - Last synced at: about 1 month ago - Pushed at: about 1 year ago - Stars: 606 - Forks: 56

mxsafiri/chatafisha-v02

Proof Of impact Market-place

Language: TypeScript - Size: 637 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

data61/PSL

Language: Isabelle - Size: 175 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 68 - Forks: 9

sarsko/CreuSAT

CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

Language: Rust - Size: 169 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 637 - Forks: 12

baro77/ZKbasicsCS

Zero-Knowledge Proofs "for (not too much :wink: ) dummies"

Size: 854 KB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 122 - Forks: 7

TimothyEarley/incompleteness

Gödels Incompleteness Theorem Proven in Arend

Size: 105 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 1 - Forks: 0

LightBurdenOfficial/SperoCoin

Sperocoin - Sustentabilidade em Tecnologia

Language: C++ - Size: 36 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 9 - Forks: 11

OpenRarity/open-rarity

Reference implementation of the OpenRarity protocol with Python.

Language: Python - Size: 9.9 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 223 - Forks: 50

iiithf/software-foundations

Software Foundations is a broad introduction to the mathematical underpinnings of reliable software.

Language: Coq - Size: 33.6 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 4 - Forks: 0

GoPlausible/.github

Plausible is a proof of anything protocol for Algorand

Size: 17.3 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 2 - Forks: 2

davidfstr/idris-insertion-sort

Provably correct implementation of insertion sort in Idris.

Language: Idris - Size: 5.86 KB - Last synced at: 3 days ago - Pushed at: about 4 years ago - Stars: 31 - Forks: 4

lemmy/lets-prove-blocking-queue

Proving a blocking queue deadlock free in a dozen different ways

Language: Dafny - Size: 123 KB - Last synced at: 24 days ago - Pushed at: 8 months ago - Stars: 42 - Forks: 5

uwplse/verdi-raft

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

Language: Coq - Size: 2.96 MB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 186 - Forks: 19

Merlin04/truthtabl.es

Truth table generator, (basic) proof builder, and more, built with Next.js and Ohm

Language: TypeScript - Size: 252 KB - Last synced at: about 15 hours ago - Pushed at: over 1 year ago - Stars: 23 - Forks: 3

seL4/graph-refine

Language: Python - Size: 1.09 MB - Last synced at: about 2 months ago - Pushed at: 3 months ago - Stars: 14 - Forks: 12

francoisschwarzentruber/prooffold

Another attempt for visualizing proofs

Language: JavaScript - Size: 1.4 MB - Last synced at: 2 months ago - Pushed at: 7 months ago - Stars: 12 - Forks: 4

aaditya29/Formal-Method-Proofs-by-Coq

Proofs in Coq

Language: Coq - Size: 45.9 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

GrahamStrickland/math_lean

Examples and exercises from "Mathematics in Lean" - Jeremy Avigad & Patrick Massot

Language: Lean - Size: 16.6 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

DistributedComponents/InfSeqExt

A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators

Language: Coq - Size: 88.9 KB - Last synced at: about 1 month ago - Pushed at: over 2 years ago - Stars: 17 - Forks: 4

DistributedComponents/disel

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

Language: Coq - Size: 1.24 MB - Last synced at: 3 months ago - Pushed at: 11 months ago - Stars: 98 - Forks: 7

Deducteam/hol2dk

HOL-Light to Dedukti/Lambdapi translator

Language: Coq - Size: 618 KB - Last synced at: 7 days ago - Pushed at: 3 months ago - Stars: 6 - Forks: 4

Deducteam/nubo

Nubo is a repository of interoperable formal proofs written in Dedukti.

Language: Makefile - Size: 124 KB - Last synced at: 3 months ago - Pushed at: about 2 years ago - Stars: 2 - Forks: 0

gallais/generic-syntax

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

Language: Agda - Size: 10.6 MB - Last synced at: 3 months ago - Pushed at: over 3 years ago - Stars: 72 - Forks: 11

discus-lang/iron

Coq formalizations of functional languages.

Language: Coq - Size: 800 KB - Last synced at: 3 months ago - Pushed at: almost 5 years ago - Stars: 143 - Forks: 8

chakravala/Math-Research-Notes

Theorems, Definitions, Papers, Research

Language: TeX - Size: 1.38 MB - Last synced at: 3 months ago - Pushed at: almost 6 years ago - Stars: 17 - Forks: 4

silvinor/bootstrap-dark 📦

The Definitive Guide to Dark Mode and Bootstrap 4 - A proof of concept

Language: HTML - Size: 3.21 MB - Last synced at: 19 days ago - Pushed at: 4 months ago - Stars: 1 - Forks: 1

DistributedComponents/verdi-lockserv

An implementation of a simple asynchronous message-passing lock server, verified in Coq using the Verdi framework

Language: Coq - Size: 58.6 KB - Last synced at: 3 months ago - Pushed at: over 7 years ago - Stars: 14 - Forks: 5

ivomac/UniquenessSpinHamiltonian

Proof of 1-to-1 correspondence between classical spin Hamiltonian spectrum and model weights

Language: TeX - Size: 1.95 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

andrew222651/semkon

LLM-based proof checker for codebases

Language: Python - Size: 73.2 KB - Last synced at: 2 months ago - Pushed at: 5 months ago - Stars: 3 - Forks: 0

kth-step/HolBA

Binary analysis in HOL

Language: Standard ML - Size: 8.28 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 35 - Forks: 21

FL45h-09/SocialHack

In this repository you can find stuff related to hack Facebook & Instagram. Disclaimer: This is only the proof of concept of my piece of code and only for educational purpose. So we are not responsible for any illegal use of this code.

Language: PHP - Size: 147 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 136 - Forks: 22

permutationlock/path_coloring_bgl

Implementations of several path coloring algorithms for the Boost Graph Library.

Language: C++ - Size: 8.62 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

RaphaelBonatti/propositional-logic-prover-python

A propositional logic prover implemented using resolution refutation.

Language: Python - Size: 43 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

janaSunrise/blockchain-python

This is a implementation of a basic blockchain structure in python, with all the description, and documentation of it's working and things.

Language: HTML - Size: 66.4 KB - Last synced at: 2 months ago - Pushed at: over 3 years ago - Stars: 15 - Forks: 9

appliedfm/vstyle

A style guide for Coq

Size: 646 KB - Last synced at: 3 months ago - Pushed at: over 3 years ago - Stars: 18 - Forks: 0

Isaac-DeFrain/dependent

An implementation of dependently typed lambda calculus

Language: OCaml - Size: 43 KB - Last synced at: 3 months ago - Pushed at: almost 3 years ago - Stars: 5 - Forks: 0

d-plaindoux/tyasta

A journey with F*

Language: F* - Size: 53.7 KB - Last synced at: 3 months ago - Pushed at: about 2 years ago - Stars: 8 - Forks: 0

paragonie/chronicle

Public append-only ledger microservice built with Slim Framework

Language: PHP - Size: 301 KB - Last synced at: about 1 month ago - Pushed at: over 3 years ago - Stars: 469 - Forks: 26

shauryashaurya/elegant

Proof checker from scratch in Python and coq / rocq

Language: Jupyter Notebook - Size: 38.5 MB - Last synced at: 3 days ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

weakmemory/imm

Intermediate Memory Model (IMM) and compilation correctness proofs for it

Language: Coq - Size: 1.52 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 23 - Forks: 3

GuilhermeStracini/POC-react-dotnet-SplitUpload

🔬 Proof of Concept of an upload split in .NET and React JS

Language: JavaScript - Size: 414 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 2 - Forks: 0

COSC3020/log-o

Size: 1000 Bytes - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

metamath/lamp-guide

Guide on how to use the metamath-lamp proof assistant

Language: HTML - Size: 22.2 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 3 - Forks: 1

beyarkay/provenance-rs

A history-of-ownership protocol to stop misinformation

Language: Rust - Size: 2.94 MB - Last synced at: about 2 months ago - Pushed at: 6 months ago - Stars: 3 - Forks: 0

xiaoshihou514/ndp.vim

Vim support for the natural deduction markup language

Language: Vim Script - Size: 18.6 KB - Last synced at: about 22 hours ago - Pushed at: 9 months ago - Stars: 0 - Forks: 0

ttwag/MAT115A-Number_Theory

Number Theory

Language: TeX - Size: 744 KB - Last synced at: 4 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0

ttwag/p13_lean4_natural_number_game_solution

Contains the solution to the natural number game in lean 4

Language: Lean - Size: 12.7 KB - Last synced at: about 1 month ago - Pushed at: 9 months ago - Stars: 0 - Forks: 0

septract/starling-tool

An automatic verifier for concurrent algorithms.

Language: F# - Size: 2.29 MB - Last synced at: 17 days ago - Pushed at: over 2 years ago - Stars: 8 - Forks: 4

denismurphy/simplified-blockchain 📦

Simplified Blockchain: A Playful Approach

Language: Rust - Size: 23.4 KB - Last synced at: 3 days ago - Pushed at: 10 months ago - Stars: 3 - Forks: 0

Monislav/Discord-Fake-Nitro-Proof-Generator

This Fake Proof generator allows you to generate an image (.png) simulating the donation of a nitro to a user. It is possible to choose by entering the ID a real user or to choose manually the name, the profile picture and the message of the user. The use of the script is done with the help of commands using Discord modals.

Language: Python - Size: 0 Bytes - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0

smorimoto/coq-to-ocaml-to-js

Proof of concept to generate safe and fast JavaScript

Language: JavaScript - Size: 402 KB - Last synced at: 8 days ago - Pushed at: almost 3 years ago - Stars: 24 - Forks: 2

deivid69e/Discord-Fake-Nitro-Proof-Generator

This Fake Proof generator allows you to generate an image (.png) simulating the donation of a nitro to a user. It is possible to choose by entering the ID a real user or to choose manually the name, the profile picture and the message of the user. The use of the script is done with the help of commands using Discord modals.

Language: Python - Size: 5.86 KB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0