Fun with Automated Proof Generation

I am always fascinated by the axiomatic foundations of mathematics and how all of it, from algebra to topology to integration theory, can be grounded ultimately in a concise list of axioms for first-order logic and Zermelo-Fraenkel set theory. Mathematics is more than just chalk on a board. It is the process of discovery. It is the revealing of an immense, elaborate structure, full of complexity and beauty. Can a theorem prover experience the joy of this discovery? Probably not. But perhaps it can help us tackle the scale. [...]

Integrated Motion Planning in Blender

Blender, MORSE, and OMPL are three very different, but related projects. The first is for 3D modeling and basic physics simulation, the second for robot control simulation, and the third for motion planning. MORSE is built around Blender, and since all three use Python APIs, there was a clear opportunity at hand. I built the interface between OMPL and the other two, allowing for a unified workflow of specifying, solving, and playing back motion paths in dynamic environments. [...]

VF-RRT Implementation for OMPL

Vector fields introduce a notion of cost to the possible solutions paths of a motion planning problem. It is expensive to move against the field, but cheap to ride it. A classmate and I contributed an implementation of the Vector Field Rapidly-exploring Random Tree algorithm to OMPL, an open-source library of robotic motion planning algorithms. [...]