Posted by: holdenlee | October 30, 2014

I am writing a novel in November.

It’s official: I am participating in NaNoWriMo (National Novel Writing Month). Here is a rough synopsis of my novel:

Money and power are useful insofar as they can change the software of society.” So wrote Ernest Oclo, an engineer-turned-programmer-turned-social theoretician, who established Functional, the first corporation-city-state. Functional –  the “control room of the world,” the producer of all the world’s algorithms – is a programmer’s dream world, where access and information is free, where everything that people created – from videogames to skyscrapers – are as modular, reusable, reconstructible as Oclos [Legos]. After Oclo, many corporations secede from a collapsing central government. Others follow their lead: those with money, those with a dream, those with loud voices all try their hands at social engineering, at creating their version of the perfect city. Each city has its own breed of people, brought up with a carefully designed culture to espouse points of view that are Babel-esque in their differences.

Linus, an orphan who grows up in Functional, and a student at Abstraction University, desires nothing more than to “contribute his little Oclos to the masterpiece of humanity” within the bubble of Functional. But change is coming. After a missionary-like trip to the Non-Programming World, he starts to see the signs: how Functional is closing up to outsiders; how the students, formerly interested in “funness,” are talking politics; how the different Programming cities are vying for power. Ernest Oclo, the original founder, has disappeared. A secret society (secrecy is unheard of in Functional!) has invited him into its ranks.

Linus’s mysterious and rich friend Zeo invites him on a trip around the world, to tour a hundred different cities. Restless, Linus accepts. Midway through the trip, however, Zeo is murdered and Linus is framed. He is labeled a Dysfunctional and prohibited from returning. Unable to return, Linus continues on the voyage that Zeo planned – though with the difficulties of having no money and his Interface confiscated. As he travels, he listens to the non-programmers are whispering about “oppression” and “rebellion,” starts to uncovers the clues behind the murder and the Society, and tries desperately to find a way to return to his beloved city and spread the alarm.

I’ve been frantically planning the story the past few days on this googledoc - which I’m making publicly commentable because I want all the feedback I can get. See the googledoc for details – there are separate pages for world, character, and plot; I’ve also listed themes I want to explore, books that inspired me, and things I need to do.

Some thoughts.

  • Why this topic? (1) I really like SF that explores different ways of thinking in depth, my favorite being Neal Stephenson’s Anathem. (2) There are a bunch of things I like about CS: I learned functional programming over the summer (will have to see how much Haskell references I can smuggle in), am reading Stephen Levy’s Hackers (I love the “Hacker ethic”), and want to build a world with that kind of culture and mindset. (So in a way, think Anathem with programmers instead of mathematicians. No way I can match that but I’d sure like to try.)
  • Why NaNoWriMo? Learn through trial by fire, anyone? I take forever to get something written, often waiting for a perfect idea that doesn’t come. I start writing things that turn into longer things and don’t get finished. This will not be an option if I want to “win” NaNoWriMo - I’ll have to not think (too much), and just write.
  • Science fiction… I love SF but am not good at writing the genre. Things I write can seem too… tame, close to the boring world of today. I’ll have to get imaginative pretty fast.
  • The NaNoWriMo community is amazing. Having a challenging common goal – write 50000 worlds in 30 days – really pulls people together and spurs meaningful interaction. For the sake of your novel, anything goes - people ask the craziest questions (Quora is a petting zoo by comparison). (The refdesk and the adoption forum are easy places to spend a lot of time perusing…)
  • Priorities: The planning I’ve been doing is also more sophisticated than anything I’ve done in advance of a piece but it’s falling far short of what I need. I have a rough setup and the bones of a plot. I need to write character sketches, come up with a history, and do more research. (Lots of places say that character is more important than plot.)
  • Give me comments. Given the 100+ hours I’ll be spending on this, your comment may make waves.
  • Especially all the CS/programming people out there: I need your input in particular! Everything from “you are doing this absolutely wrong” to “here’s a programming joke you should include!” In particular, I want to have their language resemble a programming language in some way. (Comment here, or in the googledoc, or the thread here:
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…

Older Posts »



Get every new post delivered to your Inbox.

Join 1,109 other followers