 A lot of people have been asking me what I’m going to be doing this summer, and I have been very vague, for the excellent reason that until today, I didn’t know either. I’ve been spouting buzzwords like functional programming and nlp and machine learning in every direction.
 I will be working with Prof Siddhartha Gadgil from the IISc Math Department.
 The overarching idea is to take mathematics as it is done today and rest it on the foundation of homotopy type theory (which is more scalable, so this is not as crazy as trying to do the same with set theory). This requires several steps:
 Step 1: Convert mathematics as written in papers to something controlled.
 Step 2: Translate the controlled language to HoTT
 Step 2 requires a lot of knowledge of homotopy type theory, so I’ll be working on step 1
 Step 1 has two parts
 Step 1A : Parse latex source (the typesetting languge math papers are written in – you thought they’re written in English?) and convert it into a dependency tree, which is mostly the same words, but tagged with their part of speech, and what other words they refer to.
 Fortunately there exist parsers, such as the StanfordParser, which can mostly do this for us. As Mohan Ganesalingam pointed out, mathematics is a lot easier to parse than english in general. There will be issues, of course, especially with latex formulae, but we’ll figure things out. (I hope.)
 Step 1B : Convert the dependency tree to the Controlled Language (Gadgil calls it the Naprochelike CNL, but naproche looks like English, while this stuff sure doesn’t, so I prefer to just call it Controlled Language
 The plan is to do this via a recursive functorial framework in Scala
 The framework exists, but not most of the translation rules, so my job will be to come up with these rules.
 Step 1A : Parse latex source (the typesetting languge math papers are written in – you thought they’re written in English?) and convert it into a dependency tree, which is mostly the same words, but tagged with their part of speech, and what other words they refer to.
 So now I have to quickly learn a bunch of skills
 How to program in Scala

 How to run stuff, build packages etc
 Understand what functors and monads are.

 How to use Github (I’m really embarrassed I don’t know this yet)
 How to parse English
 How to identify and describe patterns in mathematical argument.
 How to program in Scala
 And I’ve gotta read two PhD theses.
Math
Poisoned Cookies
Here’s an interesting puzzle which was part of the application for SPARC 2016. (Applications are now closed)
Suppose you have 240 cookie jars, one of which has been poisoned, so all the cookies in it are poisonous.
You also have 5 grey pigeons, each of which is immune to the poison, but has an interesting property: if it eats even a tiny crumb from a poison cookie, it will turn white at exactly 9am the following day, and stay white forever. The pigeons also have hearty appetites, and will immediately eat anything you put in front of them (which could include mixtures from multiple jars).
It is currently 8am, and you’re hosting a huge party at 10am the day after tomorrow (50 hours from now). You’d like to serve out as many cookie jars as possible while knowing, with certainty, that they are nonpoisonous.
How many cookie jars is that, and how do you know? To get full credit, you should state the maximum, explain a strategy that achieves the maximum, and then explain why the strategy is optimal. (Partial solutions that establish a large number of safe cookie jars but not the maximum will also be considered. Solutions that make erroneous arguments will be penalized, so it is better to submit a correct partial solution than an incorrect full solution.)
Think about it before you read on. This post will contain:
My Kinda Elementary but Longwinded Solution
Samyak’s Streamlined Solution
Multinomial Digression