Hoskinson Center for Formal Mathematics

hi everyone this is charles hoskinson broadcasting live from warm sunny colorado always warm always sunny sometimes colorado i'm making a quick video to talk a little bit about the hoskinson center for formal mathematics it's something that i've been working on with carnegie mellon for a little while we've been talking back and forth for several months and we finally got to announce it yesterday at a ceremony at carnegie mellon university with president farnam and the rest of the gang and anyway i just wanted to provide some commentary on it there were presentations at the center they're being processed right now and will be released on the iohk youtube channel so that people can get much more context but i just wanted to make sure that people understood what this is and how it relates to my company and cardano and other such things this is a personal donation to the center and so the point of this was to do something i was very interested in as a person it's not connected to any commercialization of cardone thus it came from my funds and it's just something i've wanted to do for the past 10 years i've been really interested in meta mathematics i've been interested in the system of mathematics the language of mathematics as much as i was interested in problems of mathematics one of the things that we have an issue with in the mathematical community is kind of three three broad problems one is over specialization which leads to a situation where a lot of work is being produced that's difficult to referee or seldom sighted or seldom read and also means cross specialization collaboration is quite difficult and there are some famous examples of this the abc conjecture proof from sunishi which has yet to be actually verified it's been out for several years and maybe right may not be right it's just simply not written in a way that anybody can actually understand it outside of a very small group of domain experts second when you look at mathematical language in the design of mathematical language when you write a proof generally speaking you have three areas of concern so one is the actual logic of deduction the the foundations you're drawing from and the process upon which you reason line by line in a linear passion a fashion to prove something and you get all the way down you say qed at the end okay so that's something that there have been hundreds of years of progress and effort good foundations like zfc and homotopi type theory and all these other things to draw from and it's a very powerful thing then there's the structure the architecture of the proof and it's kind of relating language of a software like java you have java you write a java program but a java program has an architecture it's how information flows it's the modules of it the level of modularity of it for example you write one giant monolithic proof or you could write a collection of lemmas that chained together to prove something and break things down into more manageable bits okay so that's something that there's less consensus in the mathematical community about of how to handle that that kind of design language of a proof then there's the pedagogical commentary of the proof and if your programmer this idea is like code comments and so what are the equivalent comments of proofs the proof comments and generally as an undergraduate they're extensive including many examples for example if people are trying to understand the monty hall problem if you take it from three doors to end doors and you kind of show that and run trials with it you can convince them otherwise it's very difficult to convince people with just a deductive argument about the monty hall problem okay so the pedagogical commentary is quite ample and fertile in the early days but as you go graduate level to professional mathematician it tends to evaporate a bit and that commentary also includes the thought process the heuristics used the story kind of the metadata of the proof and it's usually absent in publications and so it leaves a situation where you have something but you're not exactly sure where that thing came from so there's a lot of discussion about well how can professional mathematicians graduate students post-docs and undergraduates and those who rely upon math and its formalisms do better in general so this led to the creation of many different movements also a lot of foundational conversations about the relationship of type theory with foundations of mathematics and we saw programs like auto math mizar the qed manifesto kind of materialized from the 1970s on the problem is that while these were very interesting for a kind of an intersection of computer science in mathematics and computational logicians did great work there it was very bespoke and had very limited adoption by mainstream professional mathematicians that was until we saw a lot of traction with lean peter schultz a field medalist from germany kevin buzzard a famous professor at imperial and others are starting to use lean as a regular part of their workflow in analyzing things communicating things and a large mathematical community has formed around lean and we'll get into what lean is in just a moment but that plus the work of pioneers like jeremy avogad really said that there's an opportunity to take a step back and worry about the meta of mathematics the system of mathematics in general and if there was the right university and the right endowment there's a very good possibility that over an arc of 10 20 30 40 years that the pedagogy can be changed the approach can be changed and modern mathematicians would migrate over or the next wave of modern mathematicians would migrate over to a new system what's the point of this system well when we went from talking to each other to writing things down now you have a way of communicating thought and ideas not so powerful not not so precise but at least something with some degree of ambiguity to another party even if you're dead the problem is that your actual way you think the actual way cognition works the heuristics you use the insights you have usually that's not written down and so when you die we only get a small window into who you were what you thought for example great works of literature you can take candy from voltaire but you can't have a conversation with voltaire about that and so that's problematic well when you take mathematics and you go from just writing it down in a static language like latex that's presentation to a thinking language like lean then what you've done is you've made math machine understandable in a certain way now there are big philosophical and constructive questions of intuitionistic versus constructive mathematics and what can be written down and do we need properties like completeness and so forth for that to be effective in an agenda those are beyond the scope of this conversation however it is clear that when you make mathematics machine understandable then suddenly by interacting with the machines we write down far more than just dead text you write down the thought process the metadata that pedagogical commentary gets taken up dramatically you also have a significantly better framework for collaboration and better framework for truth because everybody can use these proofs to self-serve and if the program compiles there's a high probability that the program is correct the proof is correct that's their respect so that's really the reson detra of the lab is to look at tools like lean to look at the language of mathematics itself how math is done for the modern mathematician and to make these tools open source fully accessible and to create textbooks and and software and other things to get it into the browser to get it into everyone's hands and make math as as global as possible and as shareable as possible the presentations you'll see that are coming out especially with professor avika really tell you that the mission in a real-life usable format and i'm going to show you guys some links if you're actually curious about this so let me share my screen real quickly so first off this is lean itself and this is a project that microsoft started a few years ago leo runs it he's a brilliant guy he's got some amazing people and there's actually a interactive chat called zulupchat and there's hundreds of mathematicians currently in zulipchat and they're doing all kinds of various things with the math libraries it's a very active open source project there's an enormous amount of stuff and they're right now in the business of formalizing math with this thinking computable language you ask well what's the point there's a great paper that jeremy just published called the design of mathematical language and it kind of goes into what a semi-formal language needs to look and kind of the history of the attempts to do this like mizar and isabelle and holl light and metamath and so forth and demora's work and then there's a companion video here called the design of mathematical language where jeremy kind of walks through and explains what he's talking about in this paper so if you're really interested in this you come from a formal background a mathematical background physics background and you're thinking about adding a little more rigor or having a relationship with a computer to help you along with your research and sort some things out i'd highly encourage you go to lean click on documentation and then there's the lean manual and they're improving a lean for mathematicians in particular the center is going to be releasing a textbook called lean for mathematicians probably first second quarter of next year it just depends on how quickly jeremy and his team are going to be able to do that and a little bit about the endowment so i gave 20 million dollars to it the annualized budget is about a million a year the rest is an endowment that cmu controls and therefore they can grow that invest that which means this is a permanent center i could die tomorrow the center is going to be there for the next century two centuries it's a permanent endowment now i have every intention of continuing to add to that endowment so my goal is to grow it to an institute and i suspect around the 200 to 250 million dollar range over the next decade to two decades that's probably sufficient to ensure that this philosophy of mathematics has mainstream representation in the broader mathematical community so we'll be of course working with cmu working with that laboratory and doing everything in our power to make sure that that endowment grows to that size over time and jeremy avogad the professor is now the director of the center and so it's his job to kind of recruit the postdocs and graduate students and the students he has and starts soliciting have already achieved some pretty remarkable things for example they formalized the independence of the continuum hypothesis cohen's old proof using lean which is a rather remarkable achievement given the complexity of that and other such things so this is a slow burner it's going to take quite a bit of time probably three to five years before substantial and major results are seen but they have now permanent resources to pursue those results and hopefully because of the existence of the center it will create the right incentives for professional mathematicians to begin collaborating and adopting the tools that the center is creating and the benefit to them is that they get higher assurance that the ideas that they have are right they get more tools to explore things especially on the boundaries potentially can add new things like artificial intelligence into the mathematical game and see if that helps a little bit and also by interacting with these tools especially if they are ai driven then actually the ai's themselves will start soaking up a lot of the intuition of professional mathematicians and we'll have far more metadata a far more pedagogical commentary far more heuristic commentary about the act of doing math than just the papers themselves the constant frustration of mathematics for the last 5 000 years has always been that mathematicians die it's extremely time-consuming expensive and difficult to make a mathematician takes 10 to 15 years and then they're doing stuff and they're typically only productive in a sense maybe an additional decade to two decades when they perish a library burns to the ground and a huge amount of effort has to go into staving off this entropy as an ecosystem training the next generation of mathematicians so anything that can be done to accelerate training to accelerate collaboration to increase the set of things and to enhance the level of productivity mathematicians have for a longer period of time than just their 30s and 40s which are typically the most productive years and there's a rapid decline is extremely valuable also the ability to specialize but still have conversations with your neighbors is super important as well i also if you look at stem we continuously ask why is there not more diversity in stem usually the reason is that the skeleton key to enter the stem fields is mathematical rigor and mathematical acumen typically most educational institutions k through 12 for all communities especially the impoverished communities tend to fail in that training and so anything you can do to reduce the learning curve to acquiring mathematical skill and rigor and thought and collaboration would dramatically increase diversity in stem because once that skeleton key has been unlocked suddenly biology and chemistry and physics and astronomy and all these other fields are no longer scary for people and that's really another major component of the purpose of the laboratory tools should only be judged by their usefulness their utility their ability to evolve their durability the sustainability and of course the openness the cost of entry and these types of next generation tools that have been built on the shoulders of giants i believe very firmly as does the lab believe that can be eventually used to bring many more people into the mathematical community allow the tools of the mathematical community to to be accessed by many more fields including the softer sciences like psychology and sociology and biology and so forth and then of course advance those with much more rigor in addition to this there is one blockchain component which is this concept of inclusive accountability what makes math unique and what makes blockchains unique is usually the things we say you don't have to take on faith or authority there's a way to verify them there's a proof so when someone sends you a bitcoin or ada or ether you don't have to trust the sender if you have a copy of the blocking and the validation logic you're able to run a program and at the end of the day you'll know if what you've been sent is real legitimate the mathematical community regardless of the quality of the mathematician the background of the mathematician everyone is always treated equally in the respect that when they make an assertion of proving something there's an expectation of reproof and if one has the skills and the tools they can take that claim and self-validate self-serve and convince themselves that it's right the more accessible the validation logic is the better the community is in general and that's really the core point amongst many others so it's really been a privilege and i think it's the first thing named after me and given the size of the endowment it was a recommendation i said okay i and it's incredibly humbling and it's the privilege of a lifetime to be able to give a little bit of a push and make sure that that capital is there and that this is forever available to the mathematical community if i ever was to retire this is something that i would probably spend my retirement years on and and enjoy and do it's kind of the intersection of computer science mathematics and philosophy and logic they all come together for this particular endeavor now just some brief statements about cmu cmu is one of the most remarkable universities in the world and i've come to appreciate how special cmu is just by what we've attempted to achieve at i o global we always preach interdisciplinary research we always preach being able to build public private and government partnerships well in practice they've actually done that when you talk to a cmu faculty member it's hard to know what their background is because they sound some minutes a statistician they sound some minutes a mathematician or a physicist they sound some minutes a philosopher and when you look at the publications a lot of them are deeply interdisciplinary and there's a culture at cmu about interdisciplinary research if you're very astute you'll notice that this center is actually embedded within the philosophy group at cmu not the mathematics department or the computer science department and that's perfectly fine for cmu because of the nature of collaboration at cmu it's very easy for the mathematicians computer scientists and philosophers to simply work together and ultimately it is a philosophical question of where should mathematics go what should the philosophy of math be for the 21st century last time mathematics was reconstructed with around 1900 david hilbert many others led that so we're 120 years into this agenda and it's long overdue given that we have computers and given that world's changed a little bit and we're much more global and the internet exists to look at these domains and topics differently there are phenomenal leaders at that university that i feel incredibly comfortable with to have autonomy and vision to go and pursue this then i know that they're going to easily be able to work with the mainstream mathematical community and particularly they've demonstrated that time and again there are many nobel laureates there there are many turing fellows there and i'm just humbled and honored that i've had the opportunity to work with to give them the resources they need to get this agenda done and my job is just to get out of the way and just make sure they have what they need and they will find a way to make this happen they also have access system really phenomenal up and coming minds i had a chance to meet the graduate students who are now embedded at the center yesterday they're inc insanely bright people and i think all of them are going to have phenomenal careers in mathematics and the fact that that's going to become the standard of excellence that cmu has attracted makes me incredibly comfortable as well so if you're interested in this i'd highly encourage you read the paper i'd highly encourage you to watch jeremy's presentation on the design of mathematical language through some context and of course the videos that are going to come out about the laboratory and if you actually want to throw your hat in the ring to try to prove some things no matter your background it's a self-serve ecosystem in that you can just learn lean and interact with the community at zulu chat and they're in super friendly people and generation after generation tend to train each other there's this beautiful recursive growth that we've witnessed and hopefully five 10 15 20 years the hypothesis we have that this model was going to take off is successful but even in failure it's going to produce a lot of insight papers and brilliance so thank you so much professor avagod for becoming the director of the center thank you so much for all the members of cmu that worked with us so closely to make sure that we got that pushed away and that money is now in incredibly good hands and i'm very proud to to have gotten it where it needs to go and i can't wait to be a consumer of all the brilliance that moves in that direction so that just some brief thoughts on the center and just make sure that people understood the context of it it's not really cardano related it's not really blockchain related in any respect it's something personal for me but overall it is part of the mission of my company which is to change the systems of the world for everyone everywhere and prove them and certainly the academic system the way we collaborate the way we think the interdisciplinary nature of research that does need to be improved everybody has been desiring it but it's an incentives problem these types of centers break through and they create that type of collaboration and then inclusivity and openness which is what we've always strived for everything produced from the center should be open source and creative commons no patents at the end of the rainbow so those outputs belong to the world of today and the children who have yet to be born congratulations everybody and thank you again to carnegie mellon great organization and i look forward to seeing where things go cheers