Pinned Repositories
auto-
CDCL-Dafny
A SAT solver with nonchronological backtracking.
conky-grapes
Work on my own config files with recent conky and lua versions.
face.evoLVe.PyTorch
🔥🔥High-Performance Face Recognition Library on PyTorch🔥🔥
faceswap
Deepfakes Software For All
HOL
Canonical sources for HOL4 theorem-proving system. Branch `develop` is where “mainline development” occurs; when `develop` passes our regression tests, `master` is merged forward to catch up.
Kruskal.lean3
Reconstruction of the formalization in Lean 3.
mathlib
Lean standard library
mm-lean
One direction of the MM-Lean link
ModalTab
Verified decision procedures for modal logics in Lean
minchaowu's Repositories
minchaowu/ModalTab
Verified decision procedures for modal logics in Lean
minchaowu/mm-lean
One direction of the MM-Lean link
minchaowu/CDCL-Dafny
A SAT solver with nonchronological backtracking.
minchaowu/Kruskal.lean3
Reconstruction of the formalization in Lean 3.
minchaowu/auto-
minchaowu/conky-grapes
Work on my own config files with recent conky and lua versions.
minchaowu/face.evoLVe.PyTorch
🔥🔥High-Performance Face Recognition Library on PyTorch🔥🔥
minchaowu/faceswap
Deepfakes Software For All
minchaowu/HOL
Canonical sources for HOL4 theorem-proving system. Branch `develop` is where “mainline development” occurs; when `develop` passes our regression tests, `master` is merged forward to catch up.
minchaowu/mathlib
Lean standard library
minchaowu/formalabstracts
minchaowu/INT
Official code for paper: INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
minchaowu/Kruskal.lean
A formalization of Kruskal's tree theorem in Lean.
minchaowu/lean
Lean Theorem Prover
minchaowu/lean-client-js
minchaowu/lean-tidy
minchaowu/library_dev
Lean standard library (development)
minchaowu/mathematica
Lean-independent implementation of the MM-Lean link
minchaowu/mathematica_examples
minchaowu/minchaowu.github.io
minchaowu/o-machine
A simulation of oracle machines in OCaml.
minchaowu/PDL
Formalization of propostional dynamic logic.
minchaowu/proof-theory
Handling syntax
minchaowu/pyAudioAnalysis
Python Audio Analysis Library: Feature Extraction, Classification, Segmentation and Applications
minchaowu/Ramsey.lean
Rough formalization of Ramsey theorem in Lean. To be cleaned.
minchaowu/relevance_filter
minchaowu/TCSReadingGroup
Running efforts of a HOL reading group mechanising Michael Sipser's Introduction to the Theory of Computation.
minchaowu/temporal-logic
minchaowu/Text-2048
Text version of the 2048 game
minchaowu/youtube-dl
Command-line program to download videos from YouTube.com and other video sites