This project will contribute to the program of reverse mathematics by proving new reverse mathematics results in the area of combinatorics and by extending our understanding of the applicability of reverse mathematics to questions in constructive mathematics. The work addresses foundational questions in the mathematical sciences, specifically, -What are the limits of mathematics in advancing human knowledge.- Results will contribute to our understanding of the limits of mathematics within mathematics. By delimiting the nature and capabilities of formal reasoning, we can better understand and appreciate the potential of other, less formal means of gaining knowledge. Funding will free Hirst from teaching duties and support some travel for dissemination. Foundation support paired with sabbatical support from Appalachian State and donated summer research will provide a 14 month period devoted entirely to this research. Expected outcomes include at least two research papers on the central projects, additional related research papers, and various presentations. Two main projects are proposed. The first is extension of uniformization results that extract implications for constructive mathematics from results in reverse mathematics. The second is formalization of ultrafilter proofs of Hindman's theorem.