Posts tagged projects

Math From Scratch: Creating a Proof Checker

:: math, projects, tutorials

By: Mike Delmonaco

Math, at its core, is a network of facts that are undoubtably known to be true. We start out with some simple assumptions called axioms and prove new facts to be true using logic and reasoning. As long as the proofs are valid, then under the founding assumptions, anything that can is proven is definitely true. But when you’re proving something in math, how do you actually know if you’re doing it right? What if you make a mistake? What if you gloss over proving something which is "obviously true" that turns out to be false? One way to be sure is to have a computer check your proof, which is what we’re going to do. But first, we’re going to have to build math from the ground up.

Guess-Free Minesweeper

:: projects, game, artificial-intelligence, math

By: Mike Delmonaco

Have you ever played Minesweeper? If you have, you’ve probably run into a situation where you’re forced to guess, hoping you’re not about to step on a mine and lose the game. What if I told you it was possible to make it so you never have to guess in a game of minesweeper?

In this post, I’ll explain how I made a minesweeper solver and how I used the solver to generate guess-free minefields.

Understanding and Implementing Automatic Differentiation

:: racket, math, machine-learning, projects, tutorials, understand-and-implement

By: Mike Delmonaco

\[ \DeclareMathOperator{\expt}{expt} \DeclareMathOperator{\mul}{mul} \DeclareMathOperator{\add}{add} \DeclareMathOperator{\derivative}{derivative} \]

Automatic differentiation is a technique that allows programs to compute the derivatives of functions. It is vital for deep learning and useful for optimization in general. For me, it’s always been dark magic, but I recently thought of a nice way to implement it and made a little library. This blog post takes you along the journey of discovering that implementation. Specifically, we will be implementing forward mode automatic differentiation for scalar numbers.

This post requires some knowledge of differential calculus. You’ll need to know basic derivative rules, the chain rule, and it’d help to know partial derivatives. If you’ve taken an introductory calculus course, you should be fine.

The code is in Racket. If you don’t know Racket, you should still be able to follow along. I’ll explain the Racket-y stuff. Don’t let the parentheses scare you away!