I will present work in progress on a new foundational system for mathematics. The system is designed to make actual formalization of math--math fully written out in formal syntax--as pleasant as possible for human beings to read and write. The system involves juxtaposing ideas from the untyped lambda calculus and from set theory, along with a novel intermediating concept--definiteness--to ensure that "good" constructions are easy to carry out, while "bad" (paradoxical) constructions are illegal. I will demonstrate that the system is adequate for straightforwardly formalizing almost all of ordinary mathematics. However, I do not know whether the system is consistent. Skepticism is encouraged.