A research project in path semantics, a re-interpretation of functions for expressing mathematics

a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features

Keith Devlin's Introduction to Mathematical Thinking course on Coursera (2017 Spring)

UCalgary version of forallx, an introduction to formal logic

The Slate Interactive Theorem Prover

The lecture notes for my discrete mathematics classes.

An interpreter for Gödel's System T

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

A self-taught project about Machine Learning & Deep Learning with Python. Thanks to the countless researchers and developers around the world and their open-source code, particularly Python-based open-source code!

Human Logic

large veblen ordinal in agda

Automated mathematical theorem formulation deduced from a provided set of axioms. Builds upon the HRL theorem generator.

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

A proof-of-concept LCF-style interactive theorem prover for HOL(C)

These are my solutions to the tasks in the textbook Mathematical Logic Through Python by Nisan and Gonczarowski.

Generate Stack Math puzzles with this handy utility written in Visual Basic

HLM mathematical library for the Slate interactive theorem prover

Implementation of Russel paradox in Idris 2

first-order logic and set theory

algebra, differential equations, calculus, statistics, probability