Posted by: holdenlee | October 20, 2014

Falling leaves

(to the tune of Plastic Stars)

you ask – will you be there if I fall when I run I feel so small.
I say – it’s okay to be quite small, we don’t have to be so tall.
you say – I don’t think you see at all, do you know what follows fall
I slow – all the way down to a crawl, in my heart I feel a squall

falling leaves in a magic sylvan glen
swirling leaves where there’s one there’s always ten.

you ask – do you feel it in the air, a feeling that wasn’t there
I say – I don’t know if I would dare, I’m afraid it won’t be fair
you say – cause I really want to share, but I don’t know if you care
I slow – cause the sun is in your hair, and it’s too hard not to stare

fallen leaves in a magic sylvan glen
swirling leaves in a land without a when.


Feedback and edits welcome.

Posted by: holdenlee | September 3, 2014

Thoughts on computerized mathematics

Because “automated theorem proving” doesn’t quite capture what I want to say. I want the phrase which would fill in the blank

artificial intelligence : machine learning :: _?_ : automated theorem proving.

The analogy is that AI is what we really want, but the subject of “AI” feels like 90% speculation. “Machine learning” is that narrower field which is based upon sound mathematics/statistics, but loses those nice introspective, philosophical aspects. Computerized mathematics doesn’t seem like a winner for the blank but it’ll do for now.

I’m trying an experiment for this post: the full post is actually on workflowy. I’m writing this post in an outline format because an outline is closer to the complicated web of ideas it’s supposed to represent than linear text. There are parts which aren’t polished, and are summaries of other things. I try to connect different resources more than I explicate things myself. But the whole idea is that it’s easy to explore, you can just read the bits you want, and you can copy it and annotate it, if you’d like. Please do leave comments here.


Posted by: holdenlee | September 3, 2014

What I’ve been up to this summer

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.
Posted by: holdenlee | August 19, 2014

Talk: Proving Mathematical Theorems Using Computers

UPDATE: Code from my project (and a poster) is available at and

The slides from the talk are available at (source). I will post a more complete report when I finish my project, in about 2-3 weeks, so do check back.

Posted by: holdenlee | June 27, 2014

Analytic Class Number Formula

\displaystyle \frac{\pi}{4}=1-\frac{1}{3}+\frac{1}{5}-\frac{1}{7}+\cdots =\sum_{n=0}^{\infty}\frac{1}{4n+1}-\frac{1}{4n+3}.

I proved this identity in a post several years ago on Number Theory and Pi. It turns out that this is a special case of a more general identity called the analytic class number formula (ACNF) that evaluates an analytic quantity–a L-function at 1, L(1,\chi)–in terms of algebraic information about an extension of \mathbb Q. I have just added a chapter on the ACNF in the open-source number theory text (currently chapter 35 in the text) (source: in analytic-chapters/chapter4.tex). (Thinking in terms of L-series makes the previous proof less mysterious: fact that the number of ways to write a number as a sum of 2 squares is 4(d_1(n)-d_3(n)) falls out of an identity of Dirichlet series along with understanding how sum-of-squares relates to splitting in \mathbb Q(i).)

The ACNF also gives an identity which relates a class number to the distribution of quadratic residues modulo a prime p. In the post on prime-producing polynomials I noted that when the class number is 1, more quadratic nonresidues clump near the beginning. The ACNF gives a precise statement of this fact: for p\equiv 3\pmod 4,

h_{\mathbb Q(\sqrt{-p})}=\frac{1}{2-\left(\frac{2}{p}\right)}(R-N)

where R,N are the number of quadratic residues and nonresidues in (0,\frac p2), respectively. In other words, there are more quadratic than nonquadratic residues near the beginning, with the difference more pronounced when the class number is higher. When the class number is 1 this difference is “as small as can be.”

Read More…

Posted by: holdenlee | June 16, 2014

Nation by Terry Pratchett; The role of stories and belief

Nation by Terry Pratchett is one of my favorite books. Although nominally a young adult book, it is the most insightful novel I’ve read on the role of stories and religion/belief in our lives. On a concrete level, though, it deals with something very down-to-earth–a boy trying to figure out how to move forwards when his entire island nation is wiped out by a tsunami, a boy who thinks very honestly to himself. I’ve written up some notes on the book here. (I will add future summaries and thoughts on books that I read to


Posted by: holdenlee | June 15, 2014

Think like a child

From the podcast here:

For the short-on-time, here are highlights:

Students do much better than adults at figuring out magic tricks because they’re always asking questions and coming up with theories, while adults focus too much on one thing (and hence get misdirected by the magician), and get too wedded to arguing their theories.

What are some “childish” habits that adults can learn to adopt?

  • State the obvious.
  • Always ask questions.
  • Think small. (Often we feel like if we don’t do something “big enough” it won’t be worth it. But a small example can be remarkably insightful.)
  • Do what’s fun (cf.
    • Enjoying what you do, loving what you do is such a completely unfair advantage to anyone you are competing with who does it for a job. People who love it they go to bed at night thinking about the solutions.
    • kids [are] the research and development division of the human species. And we’re—adults—we’re production and marketing. So from the production and marketing perspective, it might look like the R & D guys are really not doing anything that looks very sensible or useful…
      But of course, one of the things that we know is that that kind of blue-sky, just pure research actually pays off in the long run.
  • Have more “diffuse” rather than focused attention.
Posted by: holdenlee | June 15, 2014

TED on collaboration

Here are some notes I took on the TED radio hour on collaboration. [Comments in brackets are my own thoughts.]

  • Jimmy Wales: Why does Wikipedia work?
    • GUY RAZ: Human motivation is driven by incentive, usually financial, and it seems like your whole model just up-ends that principle, that theory.

      WALES: Well, I don’t think so… the Internet, as a tool, allows for really brilliant people to do things that they weren’t really able to do in the past.

      One my favorite examples is to think about the best bloggers and I think the best bloggers are easily the equal of the best, say, New York Times columnist. That person always existed. 60 years ago, that person existed and all they could do, at that time, was be a, you know, fabulous person to have over for a dinner party. But now they can gain an audience of, well, maybe only a few thousand people, maybe millions of people. And they enjoy it and, you know, it is a remarkable shift in the world.

  • Luis von Ahn: Crowdsource by giving something back.
    • Some projects, like translating the Web, require an extraordinarily amount of time but can be done by many people.  To get people to help, they must be getting something out of it, or doing something they’ll have to do anyway. Duolingo is successful because it matches up an existing activity that many people want to do – learning a new language – and a problem that they could be solving at the same time as they are learning  –  translating. I.e., in return for helping translate the Web, people are learning a new language (and being recognized for it.

      [I think this paradigm has so much more potential in educational settings, because learning is the one place where people are willing to spend a lot of time, and too often people spend that time working through the exact same problems. For example, (1) in a programming class, rather than have everyone program the same thing, have everyone program different aspects of a large software project to combine together, or work on different hackathon ideas that people had come up with but not have time to carry out. (2) In a class that revolves around problem sets, and have different groups of students write up nice solutions, so that we can compile a large list of solved problems, and students can learn from the problems that they haven't done. (3) Many (math) Ph.D. programs require students to demonstrate competence in a different language by translating part of a paper. Thus we should assemble a (high-priority) list of papers/books to be translated (ex. EGA), split them up among math departments around the world, ask students to type their translations, and then put the translations together.]

      [Note: I'm actually curious as to how the CAPTCHA book-digitizing program works, because this seems to defeat the original purpose of CAPTCHAs.]

  • Clay Shirky: What motivates us to collaborate?
    • There is a large amount of cognitive surplus in the world. [Cognitive surplus is basically free time, but as I understand it, it also refers to people's desires to fill their time with intellectually meaningful work.] When people say they have no “free time,” they actually mean that their free time is already allocated. To get them to contribute to a project, we have to convince them that the work they put in is meaningful and will be recognized (i.e., we appeal to intrinsic motivations, rather than money). So we have to create environments online that appeal to those motivations.
  • Jason Freid: is too much collaboration a bad thing?
    • People can’t get work done at work because their day is shredded into many little bits. In order to work, people need time without interruptions [you need to be able to try an idea out without it being shot down immediately at a meeting]. Wikipedia, etc. works great because people can contribute on their own schedule.
  • Jennifer Pahlka: Can you code a better government?
    • Pahlka started Code for America to send programmers into government to fix problems with technology. They create apps that can be reused widely in different settings: for example, a site that crowdsources fire-hydrant shoveling in Boston could just as well be used to crowdsource tsunami-siren inspection in Hawaii. This suggests that government can work more like the Internet: (1) that people can become the “hands” of the government in working for the common interest, and (2) that one solution that works in one locality can be propagated throughout the rest of government.
Posted by: holdenlee | May 21, 2014

The Litany of Earth

The Litany of Earth is a powerfully written short story by Ruthanna Emrys, set in the world of the Cthulhu mythos but told from the other side—not the humans confronting the horrors unleashed by the cultists, but from the side of a believer. It is deeply empathetic (in a visceral way), and at the same time ponders some deep philosophical questions.

(Go read it first. Spoiler warning.)

Read More…

Posted by: holdenlee | May 20, 2014

Tai chi with Jacob

I visited my friend Jacob in Oxford this weekend. One thing about him that really inspires me is that he maintains a meditative way of being no matter what the outside world throws at him.

Tai chi in New Hall courtyard

We did tai chi together in the New Hall courtyard Sunday and Monday morning. At first he gave instructions on what to do, and I followed. (Line up the circles of your palms. Bring your hands to eye level and imagine you’re holding a wheel. Imagine there’s a beam of light going between your palms. Imagine that they are one unit. Let bad thoughts roll off your mind like water off a duck.)

At the end he said, “Now you’re the tai chi master. Tell me what to do,” and waited.

And I did.

Reflecting on this gives me an insight to the question: do you allow creative interactions between people? How do you teach people a creative art?

What did Jacob do?

  1. First, he set an example–established a set of actions and vocabulary to draw upon.
  2. Then, he set up a context of patient expectation where I had to continue, where I “can’t negate,” and just have to run with it.
  3. He stays silent and lets me be the leader, completely and without judging, so that I feel free to experiment.

Older Posts »



Get every new post delivered to your Inbox.

Join 1,108 other followers