NEAR AI Paperclub #2 AlphaGeometry: Deductive Databases, Symbolic Engines, and AI-Powered Intuition

Captions as YouTube publishes them, usually machine-generated, so product and people names can be misheard.

1. 0:00

   okay so as I said Alpha geometry is a paper that uh I was very excited about when it came out because it's uh uh it's a it's the first time I saw a very successful instantiation of uh of of the idea of having a symbolic engine doing most of the work and the model serving as something that resembles an intuition in some way I pitched this idea to many people and and people disagree with me that this counts as

2. 0:30

   intuition so it's a yeah uh I I like thinking with this intuition so let's see let's see what it means so before we dive in into anything machine learning related let's talk about DD DD stands for deductive database it's a paper from quite a while ago which was one of the I wouldn't say one of the early papers in in in attempts to solve geometry automatically I think that goes uh way way back but it's one of the uh

3. 1:04

   ones that uh directly influences output geometry the uh way the uh deductive database works is um first of all they Define a of the idea is to define a bunch of Concepts such as points circles lines angles Etc between those Concepts uh let me go slightly out of order uh for those Concepts they Define uh possible relationships uh and then they have a database of what is called uh

4. 1:38

   definite foreign Clauses which effectively say uh if certain statements are true another statement is true right and so now what you can do is you can begin like your problem statement is a set of statements right and then given your statements you can use your database of those rules uh to construct a lot of other statements and you know hopefully that will eventually lead to your uh to the actual solution to the problem you you're trying to

5. 2:03

   solve um and uh it has some caveats one caveat is that a lot of rules involve negation right so like for example I say hey points a bpq line on the same Circle uh if two angles are the same right these two and those four points are not on the same line because of four points on the same line they not on on the circle right so there's a negation that doesn't quite work with the definite horn closes because negation is usually not part of the statements you have and

6. 2:35

   they have in the in the paper they don't give a a solution that that work always they they have some heris stics that go around it but some interesting things about um about DD which Deep Mind paper inherits first one is that they use a concept of a full angle so usually when you think of an angle uh is you're thinking of uh of two rays and the angle is uh uh the the angle between them instead they define angle as two lines

7. 3:07

   uh and uh like an ordered set of lines right so so so the difference in this case is that uh these two lines can Define four different angles right and uh uh you know but the definition just says Hey the angle is those two lines if you need a specific angle you will have to specify something on top of those two lines and that simplifies a lot of things um for example you can say well

8. 3:30

   two lines are parallel you know a and CD are parallel if and only if uh the angle AB PQ right these two is equal to the angle cdpq uh if you were not using full angles that would require I think four or eight rules right because you know if C and D um are flipped right than the angle P EB would not be equal to angle P of d right so you have to you know you would have to have multiple rules but full angles is just one and they have

9. 4:02

   they have a couple other examples even in this example that we used for um uh for the for the rules you will notice that they say the angle uh PA the angle between PA and PB is equal to the angle between QA and QB but that is not sufficient rule sufficient condition if you were using angles as as as two rays because because that angle uh could be uh from A to B APB yeah you need to handle the separate

10. 4:44

    case I don't remember why anyway it it it works who's QA QB it it made more sense when I Was preparing It Anyway full angles help um okay so the actual deductive database is a set of rules there's 70 of them uh in the original database you can find the old codebase the authors eventually created a product called I think jmax uh that that has those rules and you can you can solve problems and do

11. 5:22

    things with them um so here's some examples it says hey uh you know uh if uh e is a midpoint of a and F is midpoint of AC then e f and BC are parall things like that so on top of that so so if you just use DD that can already solve quite a few problems uh but uh there are two things that are missing uh the first one still will involve no machine learning uh one of them is that sometimes you need relationships between values right

12. 5:59

    you can say hey the you know the length of uh of ab isal you know like is twice as large as some other segment or something like this uh so for that they introduce another concept called AR uh I don't know what AR stands for but effectively it's uh it's a way uh to introduce relationships between values between scalers into the uh into the mix so in this case they they uh they have three examples at the end of the paper here I have one of them

13. 6:30

    uh where they say consider the problem so the problem is on the left and then they show the approach to solving it and they first invoke DD the conductive database they say hey because we know uh that H is the X Center and because of that they get three derivations and then they say because I is the in Center they get another three derivations and so now that they have those they switch into AR where they can have where they can uh write down all the relationships and do

14. 7:02

    algebraic inference inference where they eventually conclude that b BF is equal to CJ of like a mark down language for geometrical relationships so it's so it's not necessarily so it's not so AR is not aware of the geometric nature of the of the uh of the values so for what you give to a is multiple linear equations like a system of linear equations and it solves it for you and gives you um gives you new uh

15. 7:38

    relationships between between the values and and as a matter of fact the way it works specifically uh is they have uh they build a matrix where um columns are different values uh in your in your current state of the of the problem solution right so you will you will have like some angles you will have some distances you will have some uh ratios and whatnot uh and the rows are relationships you know right so you might know that a particular segment is twice as large as another segment or uh you know like if you have uh like three

16. 8:12

    points on a line you will know that the sum of the two of the lengths is equal to the third one Etc so you you write all of them down and what you can do next is you can they they ran elimination and that allows them to have to identify other relations between between those values right so in this case they begin uh they say things like you know like let's say we have we know that a a minus B is equals B minus C right so so that means that if you move everything

17. 8:43

    to the left that would mean a minus 2 B plus C is equal to Z right A minus 2 B plus C is equal to Z and then they have another one in the third one so they write all three of them down they do Goan elimination they see that b is equal to d right that's something that deductive database would not give you no matter how many rules you apply but the go elimination allows you to to get that uh so then uh they put them

18. 9:10

    together so like in this example uh we saw an example of where they would use DD and then AR the way they put them together uh is they say they just run them one after another so they they run GD they they have a set of statements uh they run DD uh and and get all possible derivation from the database right so so DD is very fast and you know like there's there's never reason to to apply any fistic to running it they just run it to completion until it finds everything that is to be found uh once

19. 9:41

    they find everything that is to be found they build that uh Matrix run AR which is effec just a you know solving a system of linear equations that finds new relationships they put them into the set of of all the statements run DD again and they repeat it until no new that is found okay albra reasoning oh oh what stands for yeah makes sense cool now when you have DD plus a what is missing now uh is that

20. 10:20

    when you solve a problem sometimes you need to introduce a new uh point or a u construct something that does not follow from the existing uh things that you already have uh on your uh on the plane uh like you know you can look at the Circle maybe I the next slide is an example yeah so here's an example uh that's problem from one of the imos it says uh you have a triangle ABC uh and uh there are arbitrary points

21. 10:57

    d and e which are equally far from a uh and then you have um you construct BD and C yeah you look at these two segments BD and C uh and you construct the uh perpendicular here it is not drawn and the intersection of it with the circle is points G and F right and then they say well prove that D is parallel to FG it's a relatively hard problem it's a it's from myo right and uh um I have no idea how to solve it but importantly to solve it

22. 11:36

    what you need to do uh starters is you need to construct two more points m& n uh which are uh the point on the middle in the middle of the arc ab and the AC right so you construct MN uh and then once you have a m you do a lot of uh you do a lot of inference right and eventually you prove that MN is parall to D and that it's parall to GF and from that you derive that the two lines that are necessary are parallel right without being able to construct M and M you wouldn't be able to solve the problem no matter how many

23. 12:16

    times you apply deductive database and algebraic reasoning right so and the problem with the auxiliary constructions is that deductive database uh the number of rules is is finite eventually you will you will apply all the rules and and get everything constructed gion elimination is obviously Limited in time it's n cubed in the number of variables but the number of auxiliary con uh constructions you can have is obviously

24. 12:46

    unlimited right because you know you can always construct another midpoint between n and c and then midpoint between those two Etc right you can there's no limit to how many auxiliary think you can you can introduce also by the way interesting thing here to notice is that they say angle cgn is equal to C and if you look at cgn cgn and c a n you will notice that they are not equal in the in the common sense right because CGM is

25. 13:19

    a uh what is the opposite of aute F2 yes while C A is is acute right right but uh that that is the that is the reference to the fact that they use uh full angles as full angles they are equal Okay cool so how do we do those U constructions this is where machine learning comes to Aid it will be a a model that will be generating them uh so so the way it will work uh is uh they will run

26. 13:56

    ddn until they have everything that is is uh everything constructed that can be constructed and once they run out of things that can be constructed synthetic um symbolically uh if they still haven't solved the problem they go to the model and say construct something new and the model will propose a new construction and it might be useless if it's useless that's that's that's fine right because in the worst case it will just introduce

27. 14:20

    you you know more things will appear that will not be used right but as long as after multiple invocations the model does construct something you need you will solve the problem uh now the only problem is how do you teach the model to construct something useful the number of problems solved by human is very small uh it's like maybe in Geometry I think if we can get 10,000 problems that would already

28. 14:44

    be great and they will not be of the complexity necessary to solveo the way the way they do it is very interesting they they generate a very large uh synthetic data set and the way they do that is they begin by proposing uh just by constructing a bunch of random stuff right they will say hey we have two segments a and AC and they equal we have another Point D um DB and DC are equal and more over DB and C on the same line if they not on

29. 15:16

    the same line uh the first two statements can still be true right like you can imagine if I pull D below right I would still have a equal to AC and BD equal to DC but it will not be on the same line uh and then they start running um a ah so first of all the way they construct it it's not just random stuff uh instead they they construct one thing uh or rather they they might construct some random things but then they have a set of rules uh which is designed to construct things that naturally appear

30. 15:51

    in the existing problems right so this is separate from the uh deductive database this is a database for constructing aible instructions right so so this is I think as far as they go in terms of human involvement into creating this data set and so once they have those random things they start applying gdn AR uh until they construct everything that can be constructed um and once they did do that they get a random statement uh and

31. 16:22

    now you have a problem the problem says given all of that prove that this is true but here you will notice that the the fact that angle ABC is equal to angle BCA does not at all mention d right and therefore everything that has D in it can be safely removed from the set of prerequisites right so in this case the problem will say given um so so naively if you just said mention everything on top uh prove the bottom it would sound you know triangle

32. 16:54

    ABC has aals AC and D is the midpoint of BC prove that the angles are equal but everything that involves Point D can be dropped from the statement right so the problem can become uh the triangle ABC has a equ prove that the angles are equal but to prove it to prove it you do need Point d right so that point D becomes this um auxiliary construction right so so that allows you to create a

33. 17:18

    data set of uh of auxilary constructions uh interestingly the the the actual data set what it contains is uh Givens what needs to be proven and then the whole proof including all of the steps of deductive database and Al algebraic reasoning uh and so effectively it would say application of deductive database rule uh derivations from algebraic reasoning and then some construction more DD more AR struction Etc and the model is trained to predict

34. 17:56

    the whole sentence not just auxilary constructions but also uh all the output of deductive database and AR which are never used the model is only used to um to sample constructions effectively when they sample they they limit it to only being being able to sample the construction uh but according to their experiments teaching the model to do the whole solution significantly improves

35. 18:22

    her ability to to construct presumably it builds better model of the world okay so this Trace back uh Trace back where you want to get the smallest set of the of the statements or the original statements uh is not as trivial as it seems right it sounds just like you know Traverse the dag find everything that is uh that's the that's a dependency but it is not quite the case because it's not it's not a dag it's a graph that has Cycles because of the transitivity of multiple properties and they they

36. 18:56

    mention three and I suspect this set of three is exhaustive meaning that there's only three properties that introduce Loops one of them is equalities and equalities is the easiest one right so here's an example you might know that a is equal to b b is equal to c c is equal to d a is equal to e e is equal to D you want to prove that a is equal to D you can do it in two different ways you can

37. 19:18

    use the first three or you can use the last two the last two is smaller but if you're just trying to do um a back prop right if you just try to find all the dependen is uh there are Loops right because um well depending on in which order you started doing it in order to prove that a is equal to D like all all five of them will be a dependency of yours and the way they solve it for equality is relatively simple they just say well um once we

38. 19:52

    know that a is equal to B and B is equal to C we know that all of those things are equal to each other right so it doesn't make sense to keep them as five separate statements we is going to have a single vertex in the whole graph that says all of those things are equal to each other right and then when you need to prove that a is equal to d uh you can do like effectively within within this vertex you have a graph so so you know

39. 20:16

    that all of those things are equal to each other but the way you know it uh is by by having those five edges and then in that graph you can do a BFS right in order to prove that a is equal to D you might not know directly that a is equal to D but you know that because in the same vertx you know that you have a path in the graph between the vertices where vertx is is one of the scalers and an edge is an equality that

40. 20:41

    you do have a proof for right and you can use BFS to find the shortest path that's going to be your smallest set but okay I don't have a slide for it the other two uh problematic um statements are cinear right so if you have a set of points which are C like like you know a b and c on the same line and then you know b c and d on the same line then you know that all four on the same line it's a similar concept the problem is that uh you do not you cannot say like obviously

41. 21:15

    for any two points they are on the same line right so now they you don't have edges between two vertices now you have hyper edges between three vertices right you will you will know that a b and c on the same line you will know that BCD on the same line uh and and in a hyper graph with three edges you cannot run BFS moreover it's it's known to be an NP complete problem to find such a shortest path so

42. 21:37

    they use some sort of ristic and the last one is lay on the same Circle where you need at least four points so again it's a hypergraph with the four edges similarly they use theistic like a best effort attempt to find the smallest the smallest subset okay so that's for DD for ar ar is interesting you want to you run Gan elimination and you find a statement uh that b is equal to d right but but in reality in your gion like you know very deep into the

43. 22:11

    pro you will have you know 12 uh 12 scalers and something like you know 10 to 15 equations right you run go elimination and you find that two of them are equal so now you effectively you used all all 10 of them but maybe you don't need 10 of them maybe maybe there's like two or three of them which just efficient to prove it how do you find them the way they do that is uh um they say well what we can do uh is we can we can

44. 22:41

    present it as a as an attempt um like in order to prove that b is equal to D you you get each of those um rows of the Matrix multiply them by some coefficient add them up and you want to get the statement B is equal to d right so in this case what you would do is you would get um if I remember it right you would get this one oh yeah you just set X1 and X2 to um 2.5 and add them up right so A's will cancel C's will cancel B will be minus

45. 23:14

    one D will be one right d is equal to D so X1 X2 equal to 2.5 is the solution here but you cannot you cannot just minimize the number of nonzero A's that's that's a not not something that can be easily done instead they represent it in a different way they say instead of uh representing it as a single value they will represent it as a difference of two numbers Each of which is non- negative uh and then they try to minimize the

46. 23:47

    sum of those non- negative numbers such that multiplying this this ver this vector by this Matrix gives you the statement you want right uh this is uh this is all they say there are two problems with this one is that uh and they use integer linear programming so there are two problems one is that there's not always an integer solution moreover in this particular case the the solution is not integer right it's 0.

47. 24:16

    five and 0. five right so I presume they looking for an integer solution that gives you a multiple of the statement you're looking for mat will be extremely extremely SP right potentially yeah which I guess linear programming can take advantage of I don't know um the second problem here is that they are not minimizing the number of non uh nonzero x's and y's they minimize the sum of them right so here you will notice that

48. 24:47

    uh if you don't need a particular Row the optimization will always choose X and Y to be zero so that that's great that's exactly what you want uh if you want a row with a coefficient one then the mean way to achieve that is to set X to one y to Z which is exactly what we want but the problem is that sometimes you might get two rows um with coefficient one sorry two rows with a coefficient two or

49. 25:11

    one row with a coefficient three uh and then it will find you the wrong solution right because three is smaller than 2+ two Vice vers right but anyway so it's a it doesn't find you the smallest number of those values it finds you the smallest sum which presumably in many cases will will be close to what you want because coefficients usually will be around one okay uh here is a here's an example that puts all of those together I don't even want to understand the

50. 25:43

    problem statement but uh it begins so it say redundant for the constructions but they actually not not redundant it's just that you can solve the problem without introducing them but the solution that Alpha geometry comes comes with actually does use them so it uses K here uses L effectively it needs to prove that two points uh a symmetric uh relative to a particular line uh and that line is defined without that auxiliary point but it's

51. 26:14

    a it's it's it's harder to prove it that way anyway so it begins by constructing two points from the from the model and everything purple is DD green is also DD this is a r then eventually it proves it right so it's a using all three components okay um well before we go to the results one one thing is um when they when they uh when they measure it they they begin um so they assemble a data set uh the the test set the test set has all the

52. 26:57

    geometric s from IMO going back all the way I think to 2000 I'm not sure um there was a total of I think like going back 10 years like 10 years there was a total of I think 40 give or take problems of which uh some of them did not map into this Paradigm so what examples of problems that wouldn't map is any problem involving any inequality right there's no inequalities in everything we just discussed or any problem involving combinatorics because combinatorics is also out of schope right so 30 of them

53. 27:34

    did fit uh this Paradigm so 30 of them they converted and then uh just using the deductive database can solve already seven of them right so I think even that is fascinating right so out of 30 problems just applying rules can solve seven then this human design istics uh they designed by the same person who introduced deductive database he has a has a paper where he has a a set of ristics that introduce new points so those ristics

54. 28:12

    they can solve nine solve nine right so introducing algebraic reasoning brings it up to 14 and then they have an interesting um data point so so they tried GPT 4 they have a prompt uh that tried to solve problems it solves zero but then they say well it might solve zero on itself but what if we only use gp4 to create to to construct auxiliary points the same way we use our model that would be this that gives you one more problem so

55. 28:45

    not not um not massive Advantage but if they use human design characteristics that brings to 18 uh and uh as a reference it's not here in the table but I think a go medalist on average solved um 26 yeah Alpha geometry soles 25 so that's a that's a lot it didn't solve five and uh they looked at some of them I don't think I have slides for those but uh I think some of them were completely out of reach uh and for some of them it needed like it was missing constructing something but if you

56. 29:26

    introduce it it would immediately solve it is there a correlation between the problems that the humans could solve and the problems that Al can solve um that I actually don't know uh they might have mentioned it but but something interesting they mentioned is they looked at uh they looked at the number of people who Sol the problem right so complexity of the problem and how long the proof of alpha geometry is and they saw that for the three hardest

57. 29:50

    problems the three problems that were solved by barely by by by anyone the alpha geometry proofs are obscenely long right something that is definitely not a human you know human readable proof but if you remove those three from consideration then there's no correlation then it's a you know the proofs are are not the length of the proof is not relating with the with the complexity of the problem they also do a couple other things so so so they have pre-training and they have fine training so during pre-training they s they they

58. 30:21

    they train on the whole roof as I said right so including DD and AR during fine tuning they only fine tune on instructions right and so there's two more data points one says Hey what if we on the train on constructing new stuff then it's only 21 problems right so interestingly training on DD and AR is very beneficial despite the fact that they never actually use the model to predict those and without without fine tuning this s 23 right so fine tuning has

59. 30:50

    smaller impact than training than pre training so what's the difference between the model the alha geometry so Alpha geometry so so this this means they did pre-training and fine tuning yeah this one they did only fine tuning only fine tuning meaning that they only trained on constructions uh and this one is only pre-training meaning they they only trained on the full sequences never only on constructions and Alpha geometry means they trained for a while on the full

60. 31:25

    proof and then at the end they find fine tuned when they on the train only backdrop the the constructions auxilary constructions okay they have couple I I guess it's worth mentioning how they use it how they use the system the way the system is deployed is not like a single pass you know it's not just DD construction AR DD Construction in reality it's a beam search uh which uh um with a relatively large beam size

61. 31:57

    where they where they explore multiple 512 Solutions at a time uh you know and then and they have they have a variety of ablation tests not as many as one would wish but but quite a few one says that you can train on a smaller uh data set so the data set they trained on has 100 million uh proofs of those 100 million I think only 10 million actually have an auxiliary construction right so 90 million uh fully can be solved with

62. 32:27

    the GD and and AR right and if they only train on 80 million or like all the way down to 40 they only lose two problems and then they lose two more at 20 right so it's a so so this point would be very interesting to know what happens when you train on more right does it Plateau at 25 or could you get it even smarter so so that's a it would be nice to have um because of for Deep Mind scale obviously they can train on 200 million that's a that's not a question it looks like lar

63. 33:05

    right but but that's a very few data points right like presumably it has to Plateau at some point you cannot solve more than 30 it's not like between the bottom R which is 20 million and 0 it's like a 5x point I think I don't have the number of but if you compare that with the same LM St scaling law this is absolutely not there there's no log relationship in so probably yeah I mean if you if you I would rather more be interested in uh what if we can increase the diversity of

64. 33:36

    this data point and have more that require more construction instead of just 10 million out of them and probably that's more impactful than just adding more of synthetic data just kind of my but it's still interesting to see if you know if you train it on a billion does it solve one more problem or is 25 the limit yeah I I see your point on uh like Max like is there is that is that the roof but even

65. 34:00

    if that's not the roof as long as the scaling roll is linear it's kind of okay it's kind of not surprising I think we are missing the the the exponential the fact that you know the more problem you can see the more cabil gets Sol problem so I can shrink down the amount of data and I can increase the C of the of the and that's what is missing from that level y okay table B uh is a is a different uh test set it's a simpler

66. 34:32

    problems from the people who created the deductive database those more like from local local Olympiad or from textbooks there's a total of 231 Alpha geometry it solved all but three right so factly it solved almost all of them um but it's worth mentioning that they relatively like you know deductive reasoning plus algebraic sorry deductive database plus plus plus algebraic reasoning so 198 right so the data set

67. 35:02

    is not particularly challenging yeah the other two are related to beam search effectively um I I don't understand de s sufficiently deep their implementation uh to read those tables uh understand what they imply but H you mean by SE step yeah like what's the difference between the two uh I think I think I think on the late on the right one for d uh the beam size Remains the Same it's still it's always 512 yeah so so one other one other

68. 35:45

    important observation is that Alpha geometry is open source meaning that the whole code Bas is open so you can see all the rules for deductive database that they use they have some modifications to deduct active database relative to the the original one you can see all the constructions the beam search implementation everything is open okay this is the last slide that's a that's it for Alpha geometry they did publish another paper shortly after not shortly but after Alpha

69. 36:19

    geometry called Alpha proof we don't know much about that one but they did expand to uh so Alpha geometry was very interesting because uh they they did show that for geometry specifically you can have a very good symbolic representation that captures a very large percentage of problems and in which you can you can solve them but for more generic for non- geometrical problems it was not clear if that generalizes and so they built Alpha

70. 36:50

    proof is a is not using uh they not building their own Dynamic spe domain specific language anymore they're using Leen the Microsoft's uh formal verification language and then lean on the last IMO they soled four out of six problems right so they participated together with humans the same time constraints I think maybe not and the two problems they didn't solve are both combinatorics they they don't solve combinatorics yet right so Alpha proof

71. 37:21

    generalizes uh one of the problems one of the four was solved using Alpha geometry three were solved using Alpha proof Pro unfortunately is neither open source nor the user paper so we only know Basics which are effectively that you know it's kind of similar are they doing search in the space of L programs the data set is not synthetic the data set is a the way they construct it is they get

72. 37:45

    a very large number of existing math problems from Chinese Olympiad there's a million problems that are transcribed into human language and then they have an auto um a somewhat um unreliable converter from uh problem statement in in natural language into problem statement in liin but they don't care if it's not 100% correct because as long as the problem statement gets converted into something that can be solved it's still a valuable data point right and then they run a lot of search to try to solve

73. 38:20

    those and and solution would be a proof in lean you have a statement and then you have a proof and if you prove the statement link program compiles if you did not prove it it doesn't compile right so link program only compiles if every statement is proven or if you explicitly bail out on proving them but that that is easy you can say sorry sorry means trust me I'm a corgi but you can easily check presence of stories in

74. 38:44

    your code base um yeah and they so so it's it's it's it's not a synthetic data set in terms of problems but it is a synthetic data set when it comes to proofs all the proofs are synthetically generated and then they just change LM uh to predict those and then they do beam search which is a beam search paired with the with the lean parser right so beam search would only emit tokens that make sense and at every point I don't know how many of you played with Lan but the way you you do proes in Lan is that

75. 39:16

    you begin you have one goal your goal is the problem you're trying to solve and then as you go through the proof uh you can um you use So-Cal tactics and the tactics change the goal in some way like for example you can have a very very long very large goal and you can say hey it suffices to prove something else and you provide provide a different statement and now you have two goals you

76. 39:39

    need to prove that statement because you say it suffices to prove it well then you have to prove it and then you need to prove that given that the the whole goal is correct right so you have two goals uh right and so the in the link program if you if you like open it on GitHub if someone uploaded a GitHub a link program to L uh to GitHub you will not see those goals as the tactics go you will just see a set of tactics right but if you open it in an editor like

77. 40:03

    Visual Studio code or they have an line one uh and you like click into one of them you will see uh the goals at that point right and so the uh the alpha proof sees all the goals at every point right so it says hey this is my goals right now what would be the next tactic to use and it moves to the next one you mean like it reminds himself like St aligned to the right so as human you do

78. 40:27

    the same like as a human you wouldn't be just writing tactics keeping in your head what's happening right at every you would be using visual studio code right and you will see the tactics uh sorry not the tactics the goals right and then you use a tactic uh and it updates it for you right so it's a yeah so so the the the alpha proof model operates in the same environment as the human would and generally for those of you who

79. 40:51

    did not use lean lean is fascinating it's super fun uh and there's a thing called natural number game which which walks you through proving all the aoms about natural numbers like you know that addition is commutative Etc in Lin uh while teaching you Lin and it's super fun every time you prove a theum in Lin it feels like the entropy of the universe reduced and that's a that's a good

80. 41:17

    thing yeah cool yeah we we can conclude here