Lightbulb icon News Publications Showcase Talks Group Bio Awards
Headshot of Curtis
Curtis Bright

I solve mathematical problems and produce computer-assisted proofs. Using techniques from satisfiability solving and computer algebra, my work has enabled the solution of many hard combinatorial problems thousands of times faster than previously possible.

Currently, I am an assistant professor in the School of Computer Science at the University of Windsor. I completed my PhD in the Cheriton School of Computer Science at the University of Waterloo, and I hold an adjunct affiliation there as a lead of the MathCheck project.

See my curriculum vitae or bio for a summary of my academic career and my research statement, publication list, or showcase for an overview of my research. If you are interested in working with me, the MathCheck group at the University of Waterloo and the Algorithms & Mathematics group at the University of Windsor are accepting applications for open research positions.

I am currently working with two PhD students, two MSc students, three undergraduate students, and a research associate. My group's webpage lists the students I'm working with or have worked with in the past.

News

Publications

My work has been published in a number of notable venues including in the Communications of the ACM, in the Journal of Automated Reasoning, at the AAAI Conference on Artificial Intelligence 2018 (and 2019, 2021, 2022), at ISSAC 2024 (and 2018, 2011), at CASC 2016, at CASCON 2019, in the Journal of Experimental Mathematics, in the Journal of Symbolic Computation (twice), in the Annals of Mathematics and Artificial Intelligence, in IEEE Transactions of Information Theory, in Applicable Algebra in Engineering, Communication and Computing (receiving the 2020 best paper award), at ICTAI 2021, at IWOCA 2020, at IJCAI 2024 (and 2020), and appears in Maple in Mathematics Education and Research. Most of the articles are behind paywalls but preprints for each of my papers are available below if you do not have access through the publisher's site.

Writings

Copies of my academic writings in reverse chronological order. The most recent are typically co-written with students that I am supervising and may be preprints in the process of being finalized. The oldest are reports written during my undergraduate studies that I have archived as a part of my lifelong commitment to improve my writing.

Showcase

Apps, videos, and posters that I've composed to showcase my research and some of its applications. I enjoy bringing life to my research by using accessible visualizations and interactivity.

SFU 2024 seminar talk preview SAT and Lattice Reduction for Integer Factorization August 22, 2024
IJCAI 2024 poster A SAT Solver and Computer Algebra Attack on the Minimum Kochen–Specker Problem with Z. Li, V. Ganesh. August 9, 2024
AAAI 2024 poster A SAT + Computer Algebra System Verification of the Ramsey Problem R(3,8) with C. Duggan, Z. Li, V. Ganesh. February 23, 2024
AAAI 2024 poster A SAT Solver and Computer Algebra Attack on the Minimum Kochen–Specker Problem with Z. Li, V. Ganesh. February 23, 2024
Introductory Slide Dagstuhl Seminar 23161 Introductory Slide April 17, 2023
KR 2022 talk preview Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation August 3, 2022
Tutte colloquium preview SAT Solving with Computer Algebra for Combinatorics April 1, 2022
AAAI22 poster preview IP and CP Revisited for Mutually Orthogonal Latin Squares (Student Abstract) with N. Rubin, B. Stevens, K. Cheung. February 27, 2022
Dagstuhl tutorial preview Isomorph-Free Exhaustive Generation in SAT Solving (Invited Tutorial) February 17, 2022
Harvard presentation preview When Computer Algebra Meets Satisfiability: A New Approach to Combinatorial Mathematics with V. Ganesh. November 3, 2021
CanaDAM 2021 preview SAT Solvers and Combinatorics Problems May 25, 2021
Simons TV Logo Computer Algebra and SAT for Mathematical Search April 21, 2021
AAAI2021 poster preview A SAT-Based Resolution of Lam's Problem February 4, 2021
AAAI2021 opening slide A SAT-Based Resolution of Lam's Problem [full video] February 3, 2021
IJCAI2020 poster preview Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem January 14, 2021
IJCAI2020 presentation preview Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem [5 min highlights] January 6, 2021
CMS2020 presentation preview A Resolution of Lam's Problem via Satisfiability Solvers December 4, 2020
Hadamard 160 preview Hadamard 160 in Cool Tones with B. Lee. November 15, 2020
IWOCA2020 presentation preview Nonexistence Certificates for Ovals in a Projective Plane of Order Ten June 8, 2020
MC2019 presentation preview Effective Problem Solving Using SAT Solvers October 17, 2019
Colouring of the 8x8 queens graph Graph Colouring with SAT September 9, 2019
A SAT+CAS approach to finding good matrices poster A SAT+CAS Approach to Finding Good Matrices January 28, 2019
15-puzzle instance Solving the 15-puzzle December 19, 2018
Completed Sudoku puzzle Interactive Sudoku December 3, 2018
Highlighted clique of size 4 in a graph with 20 vertices Clique Finding with SAT November 15, 2018
Graeco-Latin square of order 10 Finding Graeco-Latin Squares November 7, 2018
Solution of the 8-Queens problem The n-Queens Problem October 4, 2018
Sudoku puzzle Solving the World's Hardest Sudoku October 4, 2018
Einstein with the text 'Who owns the fish?' Solving the Einstein Riddle October 4, 2018
The SAT+CAS paradigm and the Williamson conjecture poster The SAT+CAS Paradigm and the Williamson Conjecture July 17, 2018
A SAT+CAS method for enumerating Williamson matrices of even order poster A SAT+CAS Method for Enumerating Williamson Matrices of Even Order February 4, 2018
Example truth table Online Truth Table Generator May 8, 2013
Ataxx gameplay example Ataxx AI November 15, 2012
The quartic formula (cropped) The Quartic Formula [webpage] April 21, 2012
Vector rational number reconstruction poster Vector Rational Number Reconstruction April 9, 2011

Talks

An archive of my academic talks that have used slides.

Bio

Dr. Curtis Bright is an assistant professor in the School of Computer Science at the University of Windsor. He leads the development of MathCheck, a system for verifying and finding counterexamples to mathematical conjectures. His research focuses on computer-assisted proofs, automated reasoning, symbolic computation, and discrete mathematics. He received his PhD in 2017 at the University of Waterloo for demonstrating the effectiveness of combining satisfiability checking and symbolic computation for solving mathematical problems. His work on the first computer-verifiable resolution of Lam's problem won the Jacques Calmet best paper award in 2021, and in 2022 he won an Applications of Computer Algebra Early Researcher Award. In 2023, he proved the current best known lower bound in the abc conjecture.

Older history

In August 2021, I co-chaired (with James Davenport) the 2021 SC-square workshop. In the fall of 2021, I taught a graduate course on computational discrete mathematics. In the winter of 2022, and again in the summer of 2022, I taught Key Concepts in Computer Science and Introduction to Algorithms and Programming II. I taught Prog II again in fall 2022, along with a graduate course in computer algebra and computational mathematics.

In July 2021, I became an adjunct research professor in the School of Mathematics and Statistics at Carleton University. In Winter 2022, an undergraduate student I supervised, Noah Rubin, defended his Bachelor's thesis; he is now a full time software developer for Canada's cryptologic agency.

I joined the faculty of the School of Computer Science at the University of Windsor in 2020 and taught Introduction to Algorithms and Programming II in the winter of 2021.

In 2020, I held an NSERC postdoctoral fellowship at Carleton University working with professors Kevin Cheung and Brett Stevens. Our major result was generating and verifying the first set of nonexistence certificates for solving Lam's problem. In the process of our certification, we uncovered a small number of cases that had been missed in previous resolutions of Lam's problem.

Between 2017 and 2019, I was a postdoctoral fellow of the Computer Aided Research Group at the University of Waterloo. I was also affiliated with the CARGO Lab at Wilfrid Laurier University and worked with professor Ilias Kotsireas on combinatorial matrix theory. During this time, I devised the first proof that Williamson matrices exist in all orders that are powers of two.

I interned at Maplesoft in 2017 and again in 2018. While at Maplesoft I applied my research to dramatically improve some discrete optimization routines of Maple—for example, in the latest version of Maple the chromatic number of the Queen Graph of the chessboard can be computed in a few seconds instead of a few hours. I have written a number of Maple applications demonstrating how to effectively use Maple's SAT solver in a variety of problems and presented many of these applications at the 2019 Maple conference.

In March 2017, I defended my PhD thesis, supervised by Vijay Ganesh and Krzysztof Czarnecki. My thesis demonstrated the effectiveness of combining satisfiability checking and symbolic computation for solving mathematical problems.

In Fall 2015, I taught Elementary Algorithm Design and Data Abstraction alongside Gordon Cormack to 258 students. This course is the follow-up to Designing Functional Programs intended for CS and math majors and uses the programming language C.

In Summer 2015, I was the sole instructor of 145 students in Introduction to Computer Science 1, an introduction to computer science intended for non-CS majors. As the instructor I was responsible for compiling 9 assignments throughout the term and each one consisted of questions newly developed by myself.

In Fall 2014, I taught Designing Functional Programs, an introduction to computer science for CS and math majors based around the programming language Racket. I coordinated with 5 other instructors to teach 876 students.

In Summer 2014, as a part of Google's summer of code I supervised (along with William Hart) the undergraduate student Abhinav Baid and oversaw the implementation of a fast variant of the LLL algorithm for lattice basis reduction in the open source number theory library FLINT. This code is available in the latest version of FLINT in the fmpz_lll module.

In Spring 2013, I received an award for exceptional performance as an instructional assistant in the course Logic and Computation. During this term I wrote an online truth table generator for easily generating truth tables to include in assignment solutions and course notes.

In Winter 2013, I designed the SCG logo (a spoof on a proposed UW logo). At the time I was a graduate student and I've made publicly available a collection of the lecture notes that I took as a student.

In 2007, I started a personal website for nonacademic projects, though most of my effort these days goes into advancing my research program.

Awards

I won the Application of Computer Algebra Early Researcher Award at ACA 2022.

At the Maple Conference 2021 Mathematical Art and Creative Works Exhibit my submission with Bridjet Lee won the judges' choice award.

My 2020 paper A nonexistence certificate for projective planes of order ten with weight 15 codewords won the Jacques Calmet best paper award.

Bragging rights

My Erdős number is 2, through the papers Minimal elements for the prime numbers (Bright, Devillers, Shallit) and New bounds on the length of finite Pierce and Engel series (Erdős, Shallit). I have been awarded 0x$1.20 at Knuth's Bank of San Serriffe for finding a typo in The Art of Computer Programming present since the first edition (!) of volume 2 in 1969. In the 2015 version of his classic text Galois Theory, Ian Stewart cited a report of mine. Additionally, Noam Elkies once gave a talk referencing a result that I showed as an undergraduate student—the technical report is dear to my heart as one of the first papers I ever wrote.