Skip to main content

Thoughts on proof assistants

I've been long sarcastic about claims on AGI(Artificial General Intelligence). Especially on the point that humans will be someday outperformed by them in every task, will have nothing left to do, and the meaning of their lives would be destroyed permanently(Okay, you might think that this is ridiculous already, but there are some singularists actually push this scenario). Out of many reasons to maintain such an opposition, at least one argument seems clear: we humans disagree on being 'better' in general. What is a better painting? Or better music? Or better writing or research paper? As each of us humans has different and mutually exclusive answers to those questions, it seems ridiculous to me for an AGI to produce works that magically appease everyone's preferences. There surely are counterarguments against my opinion, but this writing isn't about AGI after all, so we'll move on.


My point is, on a specific task that we could measure and compare the performance of each participant, we can surely have artificial intelligence(or algorithm or model or whatever word you want to use instead of the cursed word 'Intelligence' that draws worthless attention) that is better than human. Solving arithmetic equations or literally digging a hole in the ground might be a good example. Among many well-defined measurable tasks, one thing catches my mind: proof assistant.


Mathematics is not all about proving, but mathematicians spent quite a bit of their time proving some theorem. Since the act of proving has a defined goal(building an unproven proposition or conjecture from proved theorems) and performance(time spent to finish the proof), we could propose a competition between mathematicians and a proof assistant. The good news is that we already have formal languages such as LEAN. In principle, we could just write down a conjecture using formal symbols, and wait for the proof assistant to build such a combination of symbols from the pool of already proved theorems. The bad news is, we'll have to wait for a very long time since we(and the proof assistant) have no idea what the pool looks like. What we are doing here is just comparing every known math formula to the conjecture, one by one, until we could find a magical road between the conjecture and some theorem in the pool. This ain't work.


Even more problematic is that most of our previous knowledge of mathematics isn't that formal(For example, see this). This means that many theorems out there could not be simply translated into symbols. Thus, we must first rewrite ALL of the history of mathematics in a form of some formal language. Who would do that?


But the situation doesn't seem to be overly grave in my opinion. We now have some knowledge of both NLP(Natural Language Processing) models and combinatorial search algorithms(think of AlphaGo, for example). With the continued interest of researchers, a holy grail of mathematics might not be that far.

Comments

Post a Comment

Popular posts from this blog

Transition

I came back home to spend the summer before my graduate program. There isn't much to do besides hanging out with old friends. My music production setup sits in a storage in Chicago. Research and game development also has been delayed since March; as my desktop is also in the storage, and I don't have a good working laptop right now. Well, I can still learn languages and write blog posts, I guess. Why do I write blog posts? To share new research ideas? Yes, but I find that cause overly practical. Besides, can we justify sharing all those wild imaginations and conjectures on the internet, which already suffers from a myriad of fake news? To share my life? Sure, but why would other people find my life interesting? And even if they are interested, that is not a good sign. Good people are interested in their own lives rather than the others. The reason I think is to not repeat the mistakes of the past. I don't think history repeats itself as is, but you can still often learn fro...
Post a Comment
Read more

New Album!

As I plan to move out from Chicago this summer, I am having a hard time putting efforts into my ongoing research projects. That is why I thought it is a good time to instead work on publishing the composition work I've done here. So yes, this is my first attempt at drawing an album cover, editing video clips, and so on. Plus my listening room is pretty dysfunctional as I am getting rid of my absorber blocks. I have to move out, after all. Despite all this, I hope the experience isn't too bad! I am releasing tracks one by one, hopefully a track every other week. Let's see how this turns out!
Post a Comment
Read more

20250322 Athens

  After landing at Eleftherios Venizelos Airport, I hurried to retrieve my checked-in luggage. It was my last quarter at college, so I had moved out of my apartment, shipped most of my belongings through a moving company, and brought what was left with me in a small suitcase. I had done some research beforehand, so I knew I would be taking the X95 bus to get to CYA in Πανκγράτι(Pangrati). Of course, I was advised to take a taxi, but not everyone has an extra €50 to spare. The journey started with a bit of confusion, as the airport felt vast, and I was not entirely sure where to catch the bus. I went to the information desk, where the officer directed me to the bus terminal just outside the arrivals area. Once I reached the X95 stop, I saw a long line of travelers, many of whom spoke Greek (Ελληνικά). I quickly realized the X95 was a popular choice. After tapping my card (κάρτα) and paying only €6, which was a bargain compared to the taxi, I hopped on. The bus was not exactly comfor...
Post a Comment
Read more