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 the next two years. 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 from October to December, 2017, and again in August, 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.

Previously, I delivered tutorials and assisted running courses with a focus on data structures, algorithms, and logic, receiving an award for exceptional TA performance in Spring 2013. I spent most of the decade prior to 2014 becoming well-versed in mathematics: I took over 50 courses offered by the Faculty of Mathematics at the University of Waterloo. I've also been a teaching assistant or instructor for over 20 courses.

**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. Ian Stewart cited a report of mine on computing Galois groups in the 2015 version of his text Galois Theory. 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.

Things I've (co-)written that are available online.

- June 24, 2019 SAT solvers and computer algebra systems: A powerful combination for mathematics [bib]
- June 13, 2019 Effective problem solving using SAT solvers [bib]
- May 10, 2019 Searching for projective planes with computer algebra and SAT solvers
- May 1, 2019 New infinite families of perfect quaternion sequences and Williamson sequences [bib]
- 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]
- February 26, 2019 A verifiable search for projective planes of order ten [bib]
- February 13, 2019 The best matrix conjecture
- January 28, 2019 A SAT+CAS approach to finding good matrices poster
- November 24, 2018 Complex Golay pairs up to length 28: A search via computer algebra and programmatic SAT [bib]
- September 18, 2018 A SAT+CAS approach to finding good matrices: New examples and counterexamples [bib]
- July 17, 2018 The SAT+CAS paradigm and the Williamson conjecture poster
- June 15, 2018 The SAT+CAS paradigm and the Williamson conjecture [bib]
- May 14, 2018 Enumeration of complex Golay pairs via programmatic SAT [bib, errata]
- March 19, 2018 Applying computer algebra systems with SAT solvers to the Williamson conjecture [bib]
- March 4, 2018 A doubling construction for Williamson matrices [bib]
- February 4, 2018 A SAT+CAS method for enumerating Williamson matrices of even order poster
- November 20, 2017 A SAT+CAS method for enumerating Williamson matrices of even order [bib]
- 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)
- April 27, 2017 Computational methods for combinatorial and number theoretic problems [bib, errata]
- 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]
- August 14, 2016 Searching for complex Golay sequences using a SAT solver
- July 15, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures [bib]
- February 29, 2016 PhD Research Proposal
- January 17, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures [bib]
- September 27, 2014 Minimal elements for the prime numbers [bib]
- 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]
- April 21, 2012 The quartic formula poster
- 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]
- April 9, 2011 Vector rational number reconstruction poster
- March 30, 2011 Vector rational number reconstruction [bib, errata]
- December 20, 2010 Automated construction of phylogenetic trees [bib]
- December 13, 2010 Ataxx with AI
- 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]
- February 12, 2008 NSRA on Obláth's problem
- September 12, 2007 Finding generalized near-repdigit squares

Talks I've given that used slides.

- January 30, 2019 A SAT+CAS approach to finding good matrices: New examples and counterexamples AAAI, Honolulu, USA
- October 5, 2018 SAT+CAS: A Powerful New Combinatorial Search Method Carleton, Ottawa, Ontario
- August 31, 2018 Faster SAT solving with applications to Sudoku Maplesoft, Waterloo, Ontario
- July 26, 2018 MathCheck: A SAT+CAS mathematical conjecture verifier ICMS, Notre Dame, USA
- July 17, 2018 Enumeration of complex Golay pairs via programmatic SAT ISSAC, New York, USA
- March 23, 2018 Improvements to Satisfy and ChromaticNumber Maplesoft, Waterloo, Ontario
- February 4, 2018 A SAT+CAS method for enumerating Williamson matrices of even order AAAI, New Orleans, USA
- July 29, 2017 A SAT+CAS method for enumerating Williamson matrices of even order SC
^{2}Workshop, Kaiserslautern, Germany - March 23, 2017 Computational methods for combinatorial and number theoretic problems
- 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 - September 20, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures CASC, Bucharest, Romania
- July 12, 2016 MathCheck: A math assistant combining SAT with computer algebra systems IJCAI, New York, USA
- July 2, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures SMT Workshop, Coimbra, Portugal
- May 13, 2016 MathCheck2: A SAT+CAS verifier for combinatorial conjectures ACMES, London, Ontario
- 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
- 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

- I've made publicly available a collection of the lecture notes I took as a student.
- I was the designer of the SCG logo, a spoof on a proposed UW logo.
- Nonacademic projects of mine can be found on my personal website www.curtisbright.com.