## Machine-Checked Proof

“In my view, the choice between the conventional process by a human referee and computer verification is as evident as the choice between a sundial and an atomic clock in science.” – Tom Hales (from [4])

“The rapid advance of computers has helped dramatize this point, because computers and people are very different. For instance, when Appel and Haken completed a proof of the 4-color map theorem using a massive automatic computation, it evoked much controversy. I interpret the controversy as having little to do with doubt people had as to the veracity of the theorem or the correctness of the proof. Rather, it reflected a continuing desire for human understanding of a proof, in addition to knowledge that the theorem is true” – Bill Thurston (from [6])

A machine-checked proof is a proof written in a piece of software called a ‘proof assistant’ which ensures the proof complies with the ‘axioms of mathematics’ and the rules of logic.  The question of the significance of computers in proving theorems can be polarizing (and for good reason). The quotations above represent some points of view relevant to this topic. In this post we will try answer three questions:

1. What exactly is a computer-assisted proof?
2. What are the advantages and the drawbacks of using computers to prove theorems?
3. What should an interested person do to start learning to use proof assistants?

## AMS Notices Spotlight October 2017

Hello and welcome to the October AMS Notices Spotlight. As we are now into the swing of the busyness of the semester it is sometimes nice to take a break and think about math not related to our classes. With this in mind we encourage you to take a moment out of your busy month to peruse the October AMS Notices. There are many great articles in this month’s notices including an article on Dido’s Problem, several articles on gerrymandering and many accessible articles in the Graduate student section. In addition to the great articles, there are links to the Joint Mathematical Meetings at the top of the page. This month’s featured article is an article in the graduate student section in regard to gerrymandering. Continue reading “AMS Notices Spotlight October 2017” »

## Why we need Receptive Learning to have Active Learning

In a recent issue of Notices of the AMS, Benjamin Braun, Priscilla Bremser, Art M. Duval, Elise Lockwood, and Diana White make a compelling case to include active learning in mathematics. I want to make a less popular move and ask, what is so bad about the flip side of active learning, or in other words, what’s so bad about receptive learning?

## Applying to grad school? Here’s what you need to know: Part I

I put together my grad school applications when I was studying abroad in St. Petersburg, Russia, which meant that they were cobbled together in a string of internet cafes, fueled by little more than espresso and impatience. I dashed off emails to professors in hip anti-cafes with unmarked doors and killer espresso, asking for recommendation letters and moral support. I wrote my statement of purpose over weak instant coffee (but fast Wi-Fi!) on the top floor of a mall. While I love a coffee-shop crawl as much as the next person, I was anxious to have my applications out of the way so that I could explore St. Petersburg and get to know its quirks and its grandeur.

And I did. The circumstances of my application-writing meant that I was efficient: I got things out of the way as early as I could, and as a result, I wasn’t racing to meet deadlines come December – instead, I was out and about, exploring my temporary home. On the other hand, I was not as thoughtful as I might have been in putting together my applications, and in considering what my grad school experience might look like.

While I relish the memories of my whirlwind semester abroad, here’s some advice to make your grad school application process a little less hectic­­ ­– and a little more organized ­– than mine. This is the first part of a two-part post; Part II will be posted next month. Continue reading “Applying to grad school? Here’s what you need to know: Part I” »

PROPOSITION 1:  For a real number  x  there exists a sequence $x_1, x_2, x_3,…$ of integers such that
$\hspace{4cm} x=x_1 +\frac{x_2}{2!}+\frac{x_3}{3!} + \cdots + \frac{x_n}{n!} + \cdots, \hspace{2cm} (*)$
where $x_1$ can be any integer, but for $n \geq 2$, $x_n \in \{ 0,1,…,n-1 \}.$ Furthermore, if we require that the partial sums be strictly smaller than  x, then such a representation is unique.
Remark: One cannot help recalling decimal or binary expansion of numbers. Notice that $\frac{n}{n!}=\frac{1}{(n-1)!}$ (drops back to previous digit), so the bound on $x_n$ is logical. Continue reading “Real Numbers Base…Factorials! And A By-product” »