#算法刷题#List of resources about foundational knowledge for programmers (supposed to last a few decades)
An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.
My contributions to Metamath's mmsolitaire project.
The Open Deduction Proof Editor allows proof theorists (or anyone) to deconstruction proofs step by step. It currently supports deep inference formalisms, namely Open Deduction and naturally the Calcu...
Absurdly sophisticated proofs of simple mathematical facts in Lean 4
Exploring the depths of mathematics through the study of its foundations
A webapp for creating sequent proof of propositional formulas
Parser for lambda terms, written in Haskell, that is also able to execute a list of operations on the terms
An attempt at unpacking in layman's terms what mathematics is and how it is created.
Equivalence of natural deduction and sequent calculus in HOL4
My master thesis (and related code) in Logic at the University of Bergen.
a collection of rulesets for qbar and other automated proof frameworks
Convert Proposition Trees to Conjunctive Normal Form (CNF) or Disjunctive Normal Form (DNF)
Housing useful resusable equations and formulas in calculus, discrete mathematics, and linear algebra.
My mathematical enquires