Summer 2020: looking back and looking ahead

Spring semester 2020 was a unique experience for all of us. I’m proud of my students and their efforts, both mathematical and personal, under challenging circumstances.

In January I thoroughly enjoyed the Formal Methods in Mathematics/Lean Together 2020 conference at Carnegie Mellon University. It was great to present my work and I thank the organizers for the opportunity to give a contributed talk. Here is the video.

I’m happy to report that my paper “Explicit polynomial bounds on prime ideals in polynomial rings over fields” with Henry Towsner has been accepted for publication in the Pacific Journal of Mathematics (see here for the preprint).

The future looks exciting as I forge ahead with multiple projects combining algebra, computing, and logic. Some of these extend my past work in differential algebra, proof mining, and formalization, and others head in new directions. Stay tuned!

Looking forward to Fall 2019

It’s been a productive summer and I’m excited to meet my new students as the Fall 2019 semester is about to begin here at HWS. My work on formalized mathematics is going well and I am looking forward to participating in Formal Methods in Mathematics/Lean Together 2020 (http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/) in a few months. In December I will speak at Cornell’s Logic Seminar and describe recent developments from my work on effective algebra, bounds, and proof mining. My most recent paper, “Explicit polynomial bounds on prime ideals in polynomial rings over fields”, is under review and a preprint can be found at https://arxiv.org/abs/1808.04805.

I also want to thank the organizers of the NERDS (New England Recursion and Definability Seminar) for inviting me to speak at Nerds 16.0, to be held at Bridgewater State University in November. It’s a great name and looks like a fun meeting!

Also, I am on the job market for next year and would love to discuss possibilities around formal methods, logic, algebra, and university math/CS education.

Marker 60: Pure and Applied Model Theory

I attended a special conference in honor of my thesis adviser, Dave Marker, from Oct. 25-28 at UIC (link to conference page). The talks spanned a wide range of pure and applied model theory, including talks on effective bounds in algebra (Matthias Aschenbrenner), elimination theory for difference equations (Tom Scanlon), and many others. Happy 60th, Dave!

 

Getting started at Hobart and William Smith

This fall I am starting as a Visiting Assistant Professor in the Department of Mathematics and Computer Science at Hobart and William Smith Colleges in Geneva, NY. The department has been extremely supportive and I enjoy having access to my colleagues’ expertise in commutative algebra, algebraic geometry, functional programming, etc. My students are a fun and enthusiastic group and I’m having good experiences in the classroom and with my ongoing research.

With the fall leaves starting to turn and the ever-gorgeous Seneca Lake just a stone’s throw away, I’m looking forward to a satisfying and productive semester.

Summer 2018

Summer 2018 was a busy time filled with interesting meetings and projects. I enjoyed helping celebrate Tom Hales’ 60th birthday at a meeting dedicated to Tom’s many contributions in representation theory, discrete geometry, and formalized mathematics (conference website). Many attendees work with interactive theorem provers like Coq and Isabelle and I had good conversations regarding my plans to formalize theories of polynomial rings with additional operators. Also in Pittsburgh that week was a delightful follow-up workshop organized by Jeremy Avigad at Carnegie Mellon on the theme of formal methods in control theory and dynamical systems.

Continuing the theme of formal methods, I was grateful for the opportunity to attend the 2018 DeepSpec Summer School at Princeton. The ambitious DeepSpec project seeks to build a fully verified computing system from the hardware level to the user level by employing technologies like the Coq theorem prover. I gained a deeper understanding of formal methods and I appreciate the many conversations and working sessions with other attendees and the organizers.

Association for Symbolic Logic (ASL) North American Annual Meeting in Boise

Spring was evident at the ASL meeting in Boise, ID last week (http://asl2017.boisestate.edu/). The beautiful Boise River was more than full as it rushed through the Boise State University campus where the conference was held. Thanks to the organizers for the valuable meeting and special sessions. I enjoyed my opportunity to speak in the contributed session about proof mining and its implications for differential algebra.

 

Upcoming…Ohio State University Logic Seminar March 7th

I’ll be speaking in the Ohio State University Logic Seminar on Tuesday, March 7th. Here are the details:
Title: Mining effective information from nonconstructive proofs in differential algebra
Abstract: Ultraproducts and other nonconstructive tools often yield existence results without giving explicit values. We examine the interplay of such arguments with “proof mining” techniques that systematically extract effective information even when it is not apparent. Our main application is to differential algebra, where the existence and nature of uniform bounds are more elusive than in the algebraic case. This is joint work with Henry Towsner.