There’s quite a bit to say, so I’ll just give a summary here and then elaborate on later posts as time allows.

- (Post on this now up.) I learned about proving theorems using computers. There are 2 sides to this: interactive formal verification (IFV) and automated theorem proving (ATP). I learned both the practical and philosophical aspects, read articles by Gowers, Zeilberger, etc., and talked to several people. To summarize my viewpoints,
- (1) formalization is important to further progress in mathematics because it helps “shrink the diameter of intellectual space” and offers great potential for learning mathematics,
- (2) computers have the potential to become “mathematicians’ assistants” (and perhaps even “mathematicians” themselves),
- (3) but only if mathematicians and computer scientists have some earnest discussions on problem-solving in mathematics (with some heavy introspection), we attach enough value to the formalization of mathematics, and create an environment where we can experiment with lots of programs, and
- (4) automated mathematics is a way forward in AI research.
- At the same time, my views have become more nuanced as I’ve grappled with the difficulties of the subject.

- I worked on a formal verification project.
- I formalized some basic linear algebra in Isabelle, my official project this summer (see the previous post). Unfortunately, I made rather little progress, so I was glad I spent time on learning about related subjects (see above and below).
- I started learned Coq, which I ended up finding more suited to formalizing mathematics (for reasons I’ll explain).

- I learned Haskell and Elm and fell in love with functional programming.
- I worked on implementing a theorem-prover in Haskell. It took me several weeks to do this and later I found what I’d done pretty much subsumed by Coq, but the project gave me a basic competency with Haskell, especially when I attempted to write tactics and combinators. (I’m still not satisfied with the current architecture, but I’m dropping the project until I learn enough Coq to figure out how my program should be different.)
- I feel like I can
*actually*program now. For simple things, I can stop thinking “man I wish someone had written a program to do this!” and instead, “now when am I going have time to make this program?” For instance, I made a program to infer theorem dependencies from a LaTeX document and draw a graph. Haskell does parsing–quite a messy thing–very elegantly. - Haskell is very modular (in functionality): it’s slow to start up because it takes a while to understand how to do basic things and implement them. But then you can abstract the common things that you do into some functions and then build using those functions (i.e., build using larger lego pieces). If you do it well, it’s like implementing your own higher-level language.
- Functional programming really makes transparent the similarities between mathematics and programming. (Read about the Curry-Howard correspondence.) It’s also fascinating to explore the mathematics (category theory) behind Haskell.
- More generally, I really like the way that computer programmers look at things, especially the philosophy of “ask not what your computer can do for you, but what you can do for your computer.” (More on this later.) I’ve started to get familiar with these basic things like emacs, command line, and github.

- I started learning homotopy type theory. It’s a remarkable subject because
- (1) it’s firstly a formalization of mathematics that (some weird aspects aside) seems more natural and powerful than set theory,
- (2) but unlike other logics, where it takes forever to reduce any significant mathematical theory to basic statements, significant portions of algebraic topology have been formalized within homotopy type theory and computer-checked (and in fact the process of formalization gives insight into algebraic topology).
- You can read some quite visionary remarks about HoTT in the (quite accessible) introduction to the book.

## Leave a Reply