libertasspz Goto Github PK

actuary

Formalization of the basic actuarial mathematics using Coq

adcompile

autodiff compiler

autograd

Efficiently computes derivatives of numpy code.

cofiberedingroupoids

Try to clear the `sorry`s in /LS/Deprecated/CoFiberedInGroupoids.lean

copilot-1

A stream-based runtime-verification framework for generating hard real-time C code.

copilot-verifier

System for verifying the correctness of generated Copilot programs

coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

cryptol

Cryptol: The Language of Cryptography

dalle2-pytorch

Implementation of DALL-E 2, OpenAI's updated text-to-image synthesis neural network, in Pytorch

daochenw.github.io

Website source files. Originally forked from daochenw.github.io and edited locally.

dizx

A qudit version of PyZX

lean-scheme

Schemes in Lean

lean-stacks-project

Formal verification of parts of the Stacks Project in Lean

libertasspz.github.io

My website (still in construction): LibertasSpZ.github.io

mathlib

Lean mathematical components library

mathlib4_libertas

The math library of Lean 4 (local fork)

mpl

The MaPLe compiler for Parallel ML

nisq-tda

Qiskit (python) code for Topological data analysis on noisy quantum computers

princetonalgorithms

Python implementations of selected Princeton Java Algorithms and Clients by Robert Sedgewick and Kevin Wayne

pyre-check

Performant type-checking for python.

qiskit

Qiskit is an open-source SDK for working with quantum computers at the level of extended quantum circuits, operators, and primitives.

qkd-net

Protocol stack for QKD networks with key management

saw-script

The SAW scripting language.

simuq

solvability

Viewing Graph Solvability via Cycle Consistency

sorrentum

Sorrentum is an open-Source DeFi protocol to build advanced financial applications

spectral

sqire

A Small Quantum Imperative Language for Program Verification

tensorflow

An Open Source Machine Learning Framework for Everyone

unimath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.