Curtis Bright

Postdoctoral Researcher
University of Waterloo
cbright

I am currently the lead developer of the MathCheck project of applying SAT solvers and computer algebra systems to problems in combinatorics and number theory. My work has appeared in a number of high-profile venues including the Journal of Automated Reasoning, at the AAAI Conference on Artificial Intelligence (twice), at ISSAC (twice), at CASC, the Journal of Experimental Mathematics, and in the Journal of Symbolic Computation (twice). I have been awarded an NSERC postdoctoral fellowship for two years, starting in 2020. See my curriculum vitae for a summary of my academic career and my research statement for an overview of my research.

I am currently supervised by professor Vijay Ganesh of the University of Waterloo. I am also a visiting scholar of Wilfrid Laurier University and Carleton University working with professors Ilias Kotsireas, Kevin Cheung, and Brett Stevens.

I interned at Maplesoft in 2017 and 2018. I have written a number of Maple applications demonstrating how to effectively use Maple's SAT solver in a variety of problems.

In March 2017, I defended my PhD thesis, supervised by Vijay Ganesh and Krzysztof Czarnecki.

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.

**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. 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.

Copies of my academic writings in reverse chronological order. The oldest are technical reports that are archived here as a part of my long-term commitment to improve the quality of my writing.

- September 4, 2019 A SAT certification for the nonexistence of weight 16 codewords in a projective plane of order ten [bib] submitted
- June 24, 2019 SAT solvers and computer algebra systems: A powerful combination for mathematics [bib] conference
- June 13, 2019 Effective problem solving using SAT solvers [bib] conference
- May 10, 2019 Searching for projective planes with computer algebra and SAT solvers (abstract)
- May 1, 2019 New infinite families of perfect quaternion sequences and Williamson sequences [bib] submitted
- March 20, 2019 Research statement of Curtis Bright [extended]
- March 11, 2019 The SAT+CAS method for combinatorial search with applications to best matrices [bib] submitted
- February 26, 2019 A verifiable search for projective planes of order ten [bib] submitted
- February 13, 2019 The best matrix conjecture
- November 24, 2018 Complex Golay pairs up to length 28: A search via computer algebra and programmatic SAT [bib] journal
- September 18, 2018 A SAT+CAS approach to finding good matrices: New examples and counterexamples [bib] conference
- June 15, 2018 The SAT+CAS paradigm and the Williamson conjecture (extended abstract) [bib] journal
- May 14, 2018 Enumeration of complex Golay pairs via programmatic SAT [bib, errata] conference
- March 19, 2018 Applying computer algebra systems with SAT solvers to the Williamson conjecture [bib] journal
- March 4, 2018 A doubling construction for Williamson matrices [bib]
- November 20, 2017 A SAT+CAS method for enumerating Williamson matrices of even order [bib] conference
- November 19, 2017 A new form of Williamson's product theorem [bib]
- July 11, 2017 A SAT+CAS method for enumerating Williamson matrices of even order (preprint) workshop
- April 27, 2017 Computational methods for combinatorial and number theoretic problems [bib, webpage] thesis
- December 9, 2016 New results on complex Golay pairs [bib]
- November 19, 2016 Combining SAT solvers with computer algebra systems to verify combinatorial conjectures [bib] invited journal
- September 20, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures [bib] invited conference
- August 14, 2016 Searching for complex Golay sequences using a SAT solver
- July 15, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures [bib] workshop
- February 29, 2016 PhD Research Proposal
- January 17, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures (preprint)
- September 27, 2014 Minimal elements for the prime numbers [bib] journal
- April 10, 2014 Exceptional examples in the
`abc`conjecture [bib] - April 15, 2013 Computing the Galois group of a polynomial [bib]
- April 21, 2012 The quartic formula derivation [bib, webpage]
- April 2, 2012 8*13^(4*8005)+183 is a probable prime
- December 29, 2011 From the shortest vector problem to the dihedral hidden subgroup problem [bib]
- April 20, 2011 Passing arguments: A comparison among programming languages [bib]
- March 30, 2011 Vector rational number reconstruction [bib, errata] conference
- December 20, 2010 Automated construction of phylogenetic trees [bib]
- December 13, 2010 Ataxx with AI [webpage]
- August 31, 2009 Vector rational number reconstruction
- April 29, 2009 Reduction of lattice bases [bib]
- April 16, 2009 Neural networks for insurance fraud detection [bib]
- December 15, 2008 Algorithms for lattice basis reduction
- July 20, 2008 Notes on chapter 2 of Ideals, Varieties and Algorithms
- April 24, 2008 Modular periodicity of linear recurrence sequences
- April 18, 2008 Insurance fraud statistics
- February 12, 2008 Solving Ramanujan's square equation computationally [bib, webpage]
- September 12, 2007 Finding generalized near-repdigit squares

An archive of my academic talks that have used slides.

- October 17, 2019 Effective Problem Solving using SAT Solvers [pdf] Maple Conference, Waterloo, Ontario conference
- September 10, 2019 SAT Solving with Computer Algebra: A Powerful Combinatorial Search Method UBC, Vancouver, British Columbia invited
- September 6, 2019 SAT Solving with Computer Algebra: A Powerful Combinatorial Search Method UVic, Victoria, British Columbia invited
- September 3, 2019 SAT Solving with Computer Algebra: A Powerful Combinatorial Search Method SFU, Vancouver, British Columbia invited
- July 19, 2019 Searching for projective planes with computer algebra and SAT solvers ACA, Montréal, Québec conference
- January 30, 2019 A SAT+CAS approach to finding good matrices: New examples and counterexamples [extended] AAAI, Honolulu, USA conference
- October 5, 2018 SAT+CAS: A Powerful New Combinatorial Search Method Carleton, Ottawa, Ontario invited
- August 31, 2018 Faster SAT solving with applications to Sudoku [pdf] Maplesoft, Waterloo, Ontario invited
- July 26, 2018 MathCheck: A SAT+CAS mathematical conjecture verifier ICMS, Notre Dame, USA conference
- July 17, 2018 Enumeration of complex Golay pairs via programmatic SAT ISSAC, New York, USA conference
- March 23, 2018 Improvements to Satisfy and ChromaticNumber [pdf] Maplesoft, Waterloo, Ontario invited
- February 4, 2018 A SAT+CAS method for enumerating Williamson matrices of even order AAAI, New Orleans, USA conference
- July 29, 2017 A SAT+CAS method for enumerating Williamson matrices of even order SC
^{2}Workshop, Kaiserslautern, Germany workshop - March 23, 2017 Computational methods for combinatorial and number theoretic problems thesis
- December 7, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures
- December 7, 2016 Minimal elements for the prime numbers
- November 18, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures
- September 24, 2016 MathCheck2: Combining learning-based search (SAT) with symbolic computation (CAS) SC
^{2}Workshop, Timişoara, Romania workshop - September 20, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures CASC, Bucharest, Romania conference
- July 12, 2016 MathCheck: A math assistant combining SAT with computer algebra systems IJCAI, New York, USA conference
- July 2, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures SMT Workshop, Coimbra, Portugal workshop
- May 13, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures ACMES, London, Ontario workshop
- March 14, 2016 PhD Research Proposal: A SAT+CAS system for checking math conjectures
- March 27, 2014 Extremal examples in the
`abc`conjecture - September 9, 2013 Proving the prime number theorem in an hour
- April 8, 2013 Computing the Galois group of a polynomial
- December 8, 2011 From the shortest vector problem to the dihedral hidden subgroup problem
- June 9, 2011 Vector rational number reconstruction ISSAC, San Jose, USA conference
- August 28, 2009 Vector rational number reconstruction: Version 2
- August 20, 2009 Vector rational number reconstruction
- May 21, 2009 Lattice basis reduction and the LLL Algorithm
- July 31, 2008 LLL overview: Lenstra-Lenstra-Lovász lattice basis reduction
- July 3, 2008 Notes on chapter 2 of Ideals, Varieties and Algorithms

Academic posters that I've written and designed.

- January 28, 2019 A SAT+CAS approach to finding good matrices poster conference
- July 17, 2018 The SAT+CAS paradigm and the Williamson conjecture poster conference
- February 4, 2018 A SAT+CAS method for enumerating Williamson matrices of even order poster conference
- April 21, 2012 The quartic formula poster [webpage]
- April 9, 2011 Vector rational number reconstruction poster workshop

- I've written an online truth table generator for easily generating truth tables to include on assignments.
- I was the designer of the SCG logo, a spoof on a proposed UW logo.
- I've made publicly available a collection of the lecture notes I took as a student.
- Nonacademic projects of mine can be found on my personal website www.curtisbright.com.