Zoom

Proving Patterns in Primes: The History of the Quadratic Reciprocity Law 

This presentation outlines the historical developments in the conception and solidification of the Quadratic Reciprocity Law. Starting with Fermat in the 1500s, the idea that prime numbers had patterns continued to be pondered for over 300 years later, inspiring great mathematicians such as Euler, Lagrange, Legendre, Gauss, and Eisenstein. An analysis on the techniques used by each of these to prove that certain primes always exist in certain forms naturally leads to a discussion on the Quadratic Reciprocity Law and its usefulness both at the time and in the development of modern number theory.

The Evolution of Curvature

The intuitive notion of "curvature" is a very old one, but the effort to turn this intuition into a formal mathematical concept required the work of many individuals over several centuries. In this talk, we will meet five of the major players in this story: Huygens, Newton, Euler, Gauss, and Riemann. We will see how each mathematician's theoretical contributions to curvature were intricately connected to major applied problems of their time. Finally, we will briefly journey from the work of Riemann to the modern day, exploring how these developments have shaped the current field of mathematics.

From Discrete to Continuous

 Zoom

Zahra Cheesman

Computational Complexity of the Wild Number of Edge-Labelled Graphs

This paper introduces the wild colouring of a graph, a novel concept in graph theory which was developed out of work on graphical algebraic splines. We discuss the notion of a graphical algebraic spline and revisit the seminal paper of Anders, et al, that determines when an edge-labeled graph admits only constant splines. We define the notion of the wild colouring of an edge-labelled graph and establish the computational complexity of determining whether a given edge-labelled graph with L colours has a wild edge set of size at most k. This work will help to establish a new branch of research in graph theory, while contributing to the list of known NP-hard problems and computational complexity. We further highlight the collaborative and inclusive nature of mathematical discovery, particularly the contributions of women mathematicians in this field and the value of mathematical research as a powerful avenue for social change.

Mustafa Sameen

FORMAL:  Democratizing Lean 4 Formalization Through Retrieval-Augmented Thinking and Agentic Feedback Loops

This thesis presents FORMAL (Feedback-Oriented Retrieval Method for Automated Lean translation), a novel system that automates the translation of natural language mathematical statements into formal Lean 4 code. By combining Retrieval-Augmented Generation (RAG) with an agentic feedback loop, FORMAL introduces Retrieval-Augmented Thinking (RAT), where formalized mathematics and Lean 4 proving tactics in a vector database (stored using ChromaDB) guides the generation process.
Unlike approaches that require large models or extensive cloud computing resources, FORMAL deploys relatively small, local language models (Llama 3.2 and DeepSeek-R1-8B), using Ollama, that iteratively refine outputs based on feedback from the Lean 4 theorem prover. The system incorporates tactic awareness to produce structured proofs using Lean's tactics.
The system on being evaluated on benchmarks including the FormL4 dataset, achieves 92% syntactic correctness and 86% semantic accuracy on the basic test set, compared to only 58% and 42% respectively for a pure LLM approach. The performance remains robust even on out-of-domain problems, where the system achieves 78% syntactic and 70% semantic accuracy. The agentic feedback loop is effective with most successfully formalized problems solved within just 2-3 iterations.
This work democratizes access to formal verification tools and techniques by demonstrating how contextual retrieval, tactics awareness, and compiler feedback can be used to significantly improve autoformalization without requiring a large amount of computational power. 

Zach Zerbe

Modeling Opinion Dynamics in Social Networks

In an age where we are constantly exposed to information from a variety of sources, what steps can we take to better understand the effect these sources have on the beliefs we and the peers in our social networks have? In this thesis, we explore the practicality, insights, and limitations of using mathematical models to describe belief dynamics in social networks. In particular, we use an agent-based modeling approach to the interplay between the effects of peer influence versus the influence of generally accessible information sources on various simulated network structures. We run several experiments with the model’s belief updating algorithm, and compare the results against an approximation of the system using an eigenvector based projection of system convergence. 

Tanner Flagg

Social Network Classification

Social networks have unique underlying structures that characterize the relationships they encode. Social network classification is a task that is focused on using our understanding of different networks to determine whether a network belongs to a larger one. This study discusses the structures that characterize a network and uses them to accurately classify social networks. 

Connor Wellman

Generalized Rosette Harmonic Mappings

A harmonic mapping f is a complex valued univalent harmonic function defined on a region in the complex plane. Rosette harmonic mappings are generalizations of the polynomial harmonic mappings through modifying the canonical decomposition with hypergeometric 2 F1 factors. We expand upon the Rosette Harmonic Mappings, which have analytic and coanalytic parts with exterior angles of 𝜋/2 at the nodes. By introducing a parameter q, we define Generalized Rosettes, which have analytic and coanalytic parts with exterior angles of q𝜋. For appropriate parameters, these Generalized Rosettes ‘lift’ through Weirestrauss Enneper equations to the Generalized Rosette Minimal Surfaces. At small values of q, these surfaces approximate the classical minimal surface known as Enneper’s Surface, creating a link between this classical surface and the triply periodic Rosette Minimal Surface. As q increases, the angles at the nodes of the surfaces become increasingly sharp, and the surfaces eventually become unbounded. Moreover, their projections are no longer univalent harmonic functions. By introducing a rotation angle 𝛽, with 0 ≤ 𝛽 ≤ 2𝜋, we find that seemingly unrelated Generalized Rosette Surfaces are in fact part of an associated family, suggesting they are conjugate surfaces.

 Zoom

Nathan Curl, Alana Ermeus, Arez Khidr, Karla Prado, Dylan Shryer

Scholar 2 Mentor

Scholar to Mentor is designed to streamline the mentor-matching process for Greenhouse Scholars, which is currently done entirely manually and requires significant time. Our program automates this task while maintaining the accuracy of human-made matches. By analyzing scholar and mentor applications, it identifies key similarities and returns each scholar's ideal mentor matches. This not only accelerates the process but also frees up valuable time for Greenhouse Scholars to focus on their broader mission of supporting student success in college. 

George Beck, Henry Howe, Abe Lipson, Stuart Sessions, Conor Wellman

Smart Bettor

SmartBettor.ai is a website started by a CC Alum which aims to provide users with statistics on favorable sports betting opportunities. In this project, we built out a new trends page on their website which finds trending bets and displays relevant statistics to users. This project involved refactoring old code, including the completion of a new Identity Access Management system.

Yael Homa, Evelyn Needham

SpyderBrats

Pikes Peak Performance Project: Optimization of the Spyderbat Analytics Engine

The Spyderbrat’s project aimed to enhance the performance of the Spyderbat analytics engine by leveraging the lower-level programming language Rust. Spyderbat, a cybersecurity company based in Austin, Texas, automates threat hunting by identifying the root cause of malicious events. Spyderbat’s Analytics Engine, which is written in Python, is responsible for parsing a machine’s records and mapping relevant data. When handed over to the team, it faced performance bottlenecks that limited its ability to deliver real-time threat analysis effectively. After reviewing the engine’s codebase, the Spyderbrats determined that the existing implementation was already highly optimized within the constraints of Python and Spyderbat’s design decisions. To enhance performance, they profiled the engine and rewrote critical components in Rust within the constraints of maintaining readability and the design choices of the company.

Kalie Chang, Judy Gonzalez, Grace Mun, Tori Zhu

Language Exchange

Language Exchange is a platform designed to help Colorado College students, faculty, and staff develop verbal language skills through interaction with the campus community. Due to the Block Plan at Colorado College, students often have limited time to learn and practice a language. Outside of formal language courses, there are few opportunities to maintain and improve language proficiency. Language Exchange aims to fill this gap by providing a resource for students to enhance their speaking skills while connecting with others interested in developing language skills. By fostering these connections, the platform supports students in building confidence and proficiency in their target languages.

 Zoom

George Beck

Statistics of Professional Cycling

Professional Cycling is a unique and exciting sport that combines strength, endurance, teamwork, tactics, and skills. In 2020, Zwift, a mixed-reality cycling platform, hosted a Virtual Tour de France over six weekends in the summer. There were six stages of racing each with a different course that resulted in about an hour
of virtual racing. As the professional riders raced virtually from all over the world, the outputs from their power meters were broadcast for the world to see.

This paper aims to answer two questions: What power output metrics are the most significant in describing a rider’s finish time? And, can we predict a rider’s finish time using their power metrics? The data from the Virtual Tour de France is modeled with a linear regression and multilevel models. Through our analysis, we found the peak 20-minute relative average power and the peak 15-second relative average power to be the most significant metrics. This informs us that both a rider’s ability to sustain an effort and their sprinting ability are important in mixed-reality competitions. The mean squared error and root mean squared error through 10-fold cross validation are computed to assess the predictive performance of the models. We show that multilevel models have better predictive performance than linear regression.

Kenna Grenier

Understanding the Kakeya Set

The Kakeya needle problem asks a simple question: what is the smallest possible area in which a unit-length needle can be continuously rotated through a full $360^\circ$? While simple shapes, like a circle or a deltoid triangle, seem like natural answers, more surprising constructions allow the needle to rotate in arbitrarily small regions.

We explore a construction called a Perron tree, a fragmented shape built by iteratively shifting and overlapping triangles. This peculiar structure allows a needle to turn while occupying an area that can shrink as much as we like, leading to the striking conclusion that Kakeya sets can have practically zero measure.

This raises deeper questions: If a Kakeya set can be arbitrarily small in area, what is its true dimensionality? Do their infinitely fine details give them full dimension, or are they ‘thin,’ existing in a lower-dimensional space despite their complexity? 

Hunter Markowich

Kaktovik Numerals

I will explore some mathematics from indigenous cultures, featuring counting, operations on numbers, and various applications in calendars, mapping, kinship, and other everyday concepts. I will mainly focus on the Inupiaq people of Northern Alaska, and their recently-invented number system that began as a middle school class project.
My paper will begin with a survey of the varying number systems and approaches to mathematics from different indigenous communities, and reflect on how different systems have arisen based on the applications and needs in these communities. I will also examine a specific indigenous number system: the Kaktovik numerals. Then, I will discuss what the system is used for, and how it differs from the widely-used base-10 system.
I will conclude with a closer look at how the spoken Inupiaq language links to the Kaktovik numeral symbols, in place-value, addition, subtraction, multiplication, and division.

Brendan McCune

Explorations in Category Theory

ℤThe concept of completion plays a fundamental role in mathematical analysis and algebra. The classical real numbers arise as the completion of the rational numbers with respect to the usual absolute value, but an alternative class of completions, the $p$-adic numbers, emerges when one instead considers the $p$-adic norm. This paper introduces the construction of $p$-adic integers and $p$-adic numbers as respective completions of ℤ and ℚ, with respect to the 

Porter Barnes

Topological Data Analysis of Weather Patterns

The El Niño-Southern Oscillation (ENSO) is one of the climate phenomena with the greatest impacts on weather across the globe. Though it is formally defined by average sea surface temperature (SST) increase or decreases across a large span of the Pacific, this paper investigates whether or not the shape of the sea surface temperature is also correlated to the ENSO phase. To that end, this paper introduces the fundamental concepts of Persistent Homology in order to use Topological Data Analysis to answer that question. Using Monthly mean SST data from a grid of points in the Pacific, we compute persistence diagrams for each month and ENSO phase, and then use bottleneck distances to compare those persistence diagrams. The result is clear evidence that the shape of SST data, beyond the anomaly in SST's total mean, is indicative of the ENSO Phase.

Sam Johnson

Explorations in Political Geometry, Mathematical Redistricting

Redistricting is critical in the democratic process, determining political representation by defining electoral district boundaries. However, the practice is often subject to manipulation through gerrymandering, where district lines are drawn to favor specific political parties or groups. This thesis explores computational methods for evaluating redistricting plans for partisan bias using ensemble analysis and Markov Chain Monte Carlo (MCMC) techniques.

By leveraging GerryChain, a computational tool designed for redistricting analysis, this study generates large
ensembles of districting plans to assess whether a given redistricting configuration is an outlier. A key focus is
the Recombination (ReCom) algorithm, which modifies district boundaries while maintaining contiguity and equal population constraints.

A case study of El Paso County, Colorado, is presented to demonstrate these methodologies. The analysis
compares the current districting plan against a large ensemble of possible configurations, revealing whether the
existing map exhibits signs of partisan bias. 

Zoe Harrington

Hyperbolic Tilings on Triply Periodic Minimal Surfaces

Hyperbolic tilings and triply periodic minimal surfaces (TPMS) seem to have little in common at first glance, however hyperbolic tilings can be mapped onto TPMS similarly to regular tilings on Euclidean surfaces. This project explores these connections by explaining important features of hyperbolic tilings and TPMS, delving into the specifics of orbifold symmetry notation and the tools from topology that map the tilings onto TPMS. Finally, we explore examples of hyperbolic tilings mapped onto TPMS, particularly the P-surface. Applications of TPMS range from materials science and engineering to biomineralization due to their unique structure. Many of these natural occurrences are not yet well understood by scientists, hence better understanding minimal surfaces and connections to hyperbolic geometry furthers understanding of mysterious natural and physical structures.

 Zoom

Yunus Bolat, Zahra Cheeseman, Tanner Flagg, Nick Thomas, Zach Zerbe

Caravan

Caravan is an iOS app intended to help plan and enhance the group road trip experience through its integration of real-time navigation and group coordination. Unlike existing tools that commonly isolate navigation from communication, Caravan allows users to track friends' live locations, collaboratively add and manage stops along a shared route, and plan customized trips in a centralized interface. Caravan makes road trips more organized, social, and memorable.

Luke Anderson, Jimmy Andrews, Primera Hour, Shamdeed Kabir, Mustafa Sameen

AFK

Working with the Southern Collegiate Athletic Conference (SCAC)—Colorado College’s Division III athletic conference—our team AFK (an acronym which gamers know as "Away From Keyboard") built a platform to transform Esports tracking across member schools. By combining a centralized website, database, and Optical Character Recognition (OCR), we replaced manual scorekeeping for games like Apex Legends and Valorant with a rapid screenshot-to-database pipeline. Beyond improved competitive transparency and streamlining the scoring process, our solution gives SCAC staff and players exactly what our name promises: more time "away from keyboard"—freeing them to focus on strategy, growth, and their shared passion of collegiate Esports.

Talon Carballeira, Isaac Greenwald, Sawyer King, George Sowles

Tiger One

Tiger One is a product designed to give teachers and school administrators the ability to access data on how large language models are being used in the classroom. The product consists of a chat page, which allows the student to interact with a large language model. The question and response of the student is logged in a database and displayed on the Admin page accessible by teachers. The Admin page also displays usage statistics. These statistics include usage over time, sentiment analysis, and common themes.

Kiernan Nesslar, Kazu Shimotake, Isabelle Wagenvoord

Autograder

Grading for CC Computer Science classes can be tiring, time-consuming, and just a bit obnoxious with the Canvas interface, even for very trivial assignments. This takes the time of busy professors and results in students having to wait long periods for their grades, which itself leads to piling backlogs of incomplete and incorrect assignments. CATS is a configurable command-line auto-grading program that can build custom testing pipelines for each Canvas assignment. Each time an assignment is submitted, CATS automatically downloads, performs custom tests, grades, and posts detailed feedback on student assignments to Canvas. For more subjective criteria, CATS provides output to streamline grading. CATS simplifies the grading process for all involved, saving valuable Block Plan time, and rescuing students from Week 4 headaches.

Willa Polman, Kaylie Stuteville, Ronan Takizawa, Anna Vu

AssessAI

AssessAI is a desktop software tool designed to help users evaluate and test the performance of large language models (LLMs) specifically in summarizing custom datasets. The tool allows clients to upload their datasets and assess how well various LLMs summarize their content. With this, users can determine how effectively these models could potentially serve their own projects.

AssessAI supports various popular LLM summarizers and provides evaluation metrics using BLEU, METEOR, ROUGE-Score, BERTScore, and G-EVAL. This allows for a detailed view of how each model performs, allowing the user to see which model best fits their needs.

Mira Giles-Pufahi, Oliver Kendall, Oliver Ramirez, Leigh Rose Walden, Dan Schmidt

Big Nasty

Understanding how votes add up matters. It matters for big races, but it matters for smaller, down-ballot races too. The Colorado down-ballot vote visualizer is a tool for understanding down-ballot voting trends in Colorado races. The visualization tools coloradovotevisuals.com offers are meant to lend a hand to journalists covering these races and help voters seeking more information about how support for state-level issues has changed over time. The site quickly generates three different types of visuals for any down-ballot race in Colorado that can be exported in their entirety and used in local election reporting. All the data for these visualizations comes from the Colorado Secretary of State’s elections data.

Kyle Moriarty, Oliver Moscow, Caleb Piemann

Front Range Lights

With increasing urban development and expansion previously undeveloped areas, the cultural and scientific impacts of light pollution have been studied extensively. It is true that more urban development leads to more light pollution, but quantitatively determining the amount of light pollution for any area depends on a number of factors, from the types of infrastructure present, implementation of light pollution policies, and density of light sources. Working with State of the Rockies, we believed it would be important to focus on developing a tool that would help visualize and minimize the impacts of light pollution locally. This project aims to use VIIRS data and machine learning algorithms to predict the changes in nighttime sky brightness based on the businesses and zoning data in Colorado Springs. We collected data on businesses from the ArcGIS business suite and zoning data from SpringsView. This data was used to train the model on the amount of light emitted per business so that city planners can use our tool to calculate the expected increase in light pollution when adding businesses to an area.