Posted by: holdenlee | May 1, 2015

Efficiently learning Ising models

In his paper Guy Bresler gives a new algorithm for learning Ising models. I presented this paper in Sanjeev Arora’s class on intractability in machine learning. Here are the notes from the talk.

As always, the source is available on github.

Posted by: holdenlee | March 23, 2015

The Grasshopper King, Jordan Ellenberg

(Goodreads, detailed notes)

Few books capture academia in a way that feels true – it’s easy to caricature professors into one or the other end of the spectrum: mad scientists or senile old men. The great majority of people in academia spend much of their lives adding to a small branch of knowledge. It’s hard to make them fit into any kind of dramatic story, so it’s natural to either exaggerate their contribution or make them bemoan their dusty lives wasting way.

The Grasshopper King does none of these things. It is a satire, but one that really understands academia – its author, after all, is the well-known mathematician Jordan Ellenberg. Maybe one way to describe it is as a coming-of-age in the academic world. The story takes place at Chandler State University, a no-name university that is catapulted to fame by a professor in an obscure department.

Read More…

Posted by: holdenlee | March 22, 2015

Notes on writing about books

To come soon: notes on The Grasshopper King (Jordan Ellenberg), A Passage to India (E. M. Forster).

But first, a little note, on what I’m doing with these posts on books. For most of my life, I’ve read lots of books, many of which I’ve really enjoyed but remembered very little about, and am hardly able to talk about them at all. Much in the spirit of Socrates’s quote “the unexamined life is not worth living,” I’m deciding to take notes on books I read and write a little about each one that I feel I’ve enjoyed. This means that each book may take me about twice as long to read, but it feels to me to be worth it. I may not be so detailed in the future, but I do want to capture my thoughts for each book. (I listened to Moonwalking with Einstein recently, which raises these questions in a much deeper way – but that’s another post.)

There’s two halves to this notetaking and writing. One part is (a) simply recording summaries and quotes (perhaps with brief notes) indexed into the book, and the other is (b) a post on my thoughts.

Firstly, making chapter/page notes on workflowy (a) will hopefully, make everything that was significant to me in the book easily indexable. My secret hope is that other people will do this, and there will be a whole library of these “indexed summaries/quotes/impressions” online, so that we can much more easily draw upon ideas, feelings, and quotes from books (or movies, etc.) in our conversations, as well as compare different people’s responses side by side. (This is the basic idea of the “backchannel” idea I had, adapted to books – I would love for such a site to exist. It would be like opening up a book and finding that the previous reader had left a bunch of post-it notes inside on their thoughts – but this for everyone who logs their thoughts on the site.) Notes aren’t meant to be a replacement for the book itself, more like a way to remember it without rereading it. I don’t think this is prevalent idea at all – there are terse summaries of books, and there is the book itself, and there are literary essays which are a bit detached, but nothing in the middle.

(b) My posts aren’t so much reviews – they’ll pretty much spoil the most important parts of the plot – but rather me trying to get to the essence of what the book is saying to me, and how I think about it. There’ll be lots of quotes, because nothing captures the essence of a book better than quotes from the actual books. They’re not going to be like literary essays. Books, I think, are meant to be taken in the context of life, so I’ll write about what it suggests about love, faith, death, whatever.

How to read these posts? Two ways, I think. One is to read the book yourself, and then read my post to see what someone else thought and remembered about it, to compare with your own thoughts. Another is to say, I don’t have time to read this book, so I’m just going to read this post. There’s many more books than I have time to read, and it seems a winning proposition for people to write down these essences of books to communicate.

Importantly, the posts aren’t a factual summary (which by itself would be hard to remember anyway). To me, the more important thing is to try and capture what the book meant to me, the thoughts and questions that it brought up in my head, the kind of things I would want to talk about in a discussion on the book. The filler material between the quotes from the book will be my own interpretation of things, which should be taken to be “in the world of the book as it exists in impressions in my head.” One thing that keeps people from talking about books more, I think, is that English class encourages a certain kind of literary analysis, giving the impression that intelligent discussion has to involve this kind of literary analysis, when it can, and should, I think, simply start with one’s feelings about the book. Books make us all feel, therefore we can talk about them.

Anyway, if all works out I’ll keep writing these. So I would love to have discussions of this process, how these posts/notes might work better! It’s working for me so far, but I don’t know if anyone else thinks they’re useful in the way I describe.

Posted by: holdenlee | March 21, 2015

Justine, Lawrence Durrell

It’s a book about the contradictions of love, but unlike any I’ve seen before. The prose is exquisite, wounding, some of the most powerful I’ve seen. It feels impossible to put any sort of frame around it. The story shifts forwards an back in time (in the narrator’s words, the events are “not in the order in which they took place — for that is history — but in the order in which they first became significant for me”) so that plot can be hard to follow, but read it for the prose. It speaks for itself, so I’ve compiled a long list of quotes/notes. I won’t reach any kind of conclusion, but rather try to order my thoughts about a very chaotic novel, try to fold the events in the story together, to see the beginnings and the ends brought together through the intervening pages. Nah, actually, this post is more like throwing a bunch of quotes onto the page. They speak too strongly for themselves.

A small group of people, perambulating, interact with each other in Alexandria. The city is a character; it influences their actions and weighs heavily on their minds. The narrator and his lover Justine try to explain what they desire, explain the contours of love, justify their own actions, find some pattern the way their feelings shift. In these attempts they form hundreds of absurd but striking hypotheses that form the patchwork of the novel – because the most powerful quotes about love are not those that reach a sensible conclusion, but those utterances born out of passion, despair, confusion, and false enlightenment, a desire to make sense of things.

Read More…

Posted by: holdenlee | March 8, 2015


Starting up this blog again! I’ll begin by writing about a few books I’ve read in the past few months that I’ve really enjoyed. I’m also starting a habit of taking notes on the books I like and making them available at I’ll post detailed summaries/page notes there and write freely about my impressions on my blog. (For this book:

When I meet someone new, I like to ask them for book recommendations. This is how I came across Byzantium by Stephen Lawhead. Historical fiction is not a genre I’ve read much in, but this definitely makes me want to read more. It’s an epic adventure full of twists and turns and at the same time very thought-provoking.


(taken from

Although born to rule, Aidan lives as a scribe in a remote Irish Monastery on the far, wild edge of Christendom. Secure in work, contemplation, and dreams of the wider world, a miracle bursts into Aidan’s quiet life. He is chosen to accompany a small band of monks on a quest to the farthest eastern reaches of the known world, to the fabled city of Byzantium, where they are to present a beautiful and costly hand-illuminated manuscript, the Book of Kells, to the Emperor of all Christendom.

Thus begins an expedition by sea and over land, as Aidan becomes, by turns, a warrior and a sailor, a slave and a spy, a Viking and a Saracen, and finally, a man. He sees more of the world than most men of his time, becoming an ambassador to kings and an inmate of Byzantium’s fabled Golden Court. And finally this valiant Irish monk faces the greatest trial that can confront any man in any age: commanding his own Destiny.

Spoiler warning!

Read More…

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.

Older Posts »



Get every new post delivered to your Inbox.

Join 1,196 other followers