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 | 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 | August 19, 2014

## Talk: Proving Mathematical Theorems Using Computers

UPDATE: Code from my project (and a poster) is available at https://github.com/holdenlee/Isabelle and http://afp.sourceforge.net/entries/VectorSpace.shtml

The slides from the talk are available at https://dl.dropboxusercontent.com/u/27883775/math%20notes/IFV.pdf (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.”

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 http://bit.ly/hlbooklist.)

Posted by: holdenlee | June 15, 2014

## Think like a child

For the short-on-time, here are highlights:  http://marker.to/Aa8do7

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.

• State the obvious.
• 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. http://holdenlee.wordpress.com/2013/04/11/learning-should-be-fun/)
• 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? http://marker.to/tWIjjf
• 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. http://marker.to/XYEFWk
• 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? http://marker.to/9hTGCX
• 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? http://marker.to/YUtOgb
• 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? http://marker.to/x8Um0v
• 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.)

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.

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.
Posted by: holdenlee | May 16, 2014

## Weekly summary, 5-16-14

I’m starting a weekly post where I write about or link to some interesting articles I’ve read or interesting podcasts I’ve listened to in the past week (just podcasts for this week). I’ve tried a few new podcasts (and also continued my staples of Radiolab, 99% invisible, This American Life).

99% invisible

• 109 Title TK: Naming is so important that there are companies that specialize in it. There’s a spectrum of naming, from descriptive names like “Raisin Bran” to suggestive names to abstract names (empty vessels) like “Kodak.” Two companies have different philosophies: one come up with thousands of names (and analyzes them linguistically), the other focuses on a few at a time and focus on choosing names that tell a story.
• 110  How the Citicorp building was built on stilts, how an undergraduate architecture student noticed a critical flaw, and how they repaired it while keeping all the building’s residents were completely oblivious to the danger.

Freakonomics

I don’t know (transcript); on the virtues of experimentation: Many people would try to BS an answer to a question rather than admit that they don’t know. This is especially true when talking to higher-ups.

One of the first steps in learning to think like a freak is learning to say “I don’t know.” Why? Because until you can admit what you don’t know, it’s virtually impossible to learn what you need to. Because if you think you already have all the answers, you won’t go looking for them.

…the only way to learn is through feedback. That whether you’re a human being, an animal or an organization, the way that you learn is by trying different things and seeing the outcome when you try different approaches, and comparing those outcomes.

The way to do this is by experimentation. While people would agree in theory that experimentation is a good idea, Levitt found that the pressure to “be an expert” means they don’t actually put it into practice:

But in order to be willing to run the experiment you have to say, well, geez, I don’t know the answer. Wait, but you are the expert. You are in charge of marketing. You are in charge of pricing. You are supposed to know the answer. And so the people in the firms we were working with felt so much pressure to be the expert that they wouldn’t run the experiments because that was an admission that they weren’t really as expert as they maybe had been pretending to be or as other people wanted them to pretend to be.

They give one example: A company was spending millions of dollars on paper ads without knowing whether they were effective. When Levitt suggested they try advertising in 20 cities and not advertising in 20 cities as an experiment, the ad department told him, “Are you crazy? We’d all get fired.” They told the story of how one guy forgot to run ads in Pittsburgh and got fired. But then they looked back at the sales records and found that actually, the failure didn’t decrease the sales.

How do we change? The best thing is for people at the top of the hierarchy to establish a culture of “I don’t know, but it would be good to find out.” But doesn’t happen often, as many people got up there by pretending to know in the first place.

[Some of my own rambling thoughts: Experimentation requires time and space, and not being judged moment to moment. You have to take a long-term view; for instance, taking the time to ascertain what doesn't work wastes time in the short run (and would get you criticized if you're being followed too closely) but will save time in the long run because you have a definite rather than fuzzy idea of how different approaches compare. I think a lot about how to allow more "experimentation" into my life (because I'm really not that good at it unless I feel there's an explicit context set up for it), a lot of it seems to be the mindset of not caring what's awkward or graceful* in the moment, but keeping a longer view in mind, and also starting things long before an obligation to perform (e.g. a due date) sets in.]

*From a previous episode of The Moth: People in this generation think about what’s awkward and graceful, in the parents’ generation think about what’s appropriate and inappropriate, and from the grandparents’ generation think about what’s moral and immoral.

Brand over brain: When we buy certain brands, we’re buying into the experience of the product, or the “dream” behind the product, ex. Apple is more creative (See also Predictably Irrational (Ch. 9-10); our expectations influence our experiences). We dismiss advertisers as manipulative, and want instead to observe some objective measure of quality, but experience is itself subjective. It’s good to understand the psychology behind this experience, and how our beliefs shape it.

• Spurlock talks about a documentary about product placement that is itself fully of product placements.
• Bloom argues that we are “essentialists,” forever trying to find the origin, stories, and hidden nature of the things around us, and taking pleasure in doing so.
• Pine defines authenticity. It’s knowing the origin of something and being able to feel it. (For instance, Starbucks does this well because it tells you where the beans are from, and you can even feel them in your hands in the shop.) Authenticity has to feel rooted in place, and ubiquity goes against the grain. Authenticity is not the same as reality: Disneyland is a fake, manufactured reality but an authentic experience because it stays true to a certain dream. Because our feelings shape our experiences, authenticity is a worthwhile pursuit.
• Sutherland argues that lots of problems can be solved if we simply improve the attractiveness of certain actions or products change people’s perceptions of  rather than the products themselves – getting people to take their antibiotics by coloring the 6 of 24 blue and telling them to take those last, for instance; or making “impulsive spending” a thing. There’s a discussion of the placebo effect.

Quotes from the end:

Poetry is when you make new things familiar and familiar things new, which isn’t a bad definition of what our job is – to help people appreciate what is unfamiliar, but also to gain a greater appreciation and place a far higher value on those things which are already existing.

We are perishing for want of wonder, not for want of wonders, which, I think, for anybody involved in technology, is perfectly true.

Some cool examples throughout: getting children to eat carrots and milk by saying they’re from McDonald’s; making adults like wind more by putting it in a fancy bottle; Germany getting its people to eat potatoes by only allowing the nobility to grow it but not guarding it too closely, so that people will steal it and want it (cf. Predictably Irrational Ch. 2).

Follow