00:00:00: And this is really, really dangerous because it's going to mean that the space for inquiry gets closed down.

00:00:08: Because people think they know the answer but don't what we're talking about?

00:00:11: That not good!

00:00:12: To me Claude as like a twenty-six year old precocious PhD student you know throws off works hard does lots of things talks crap quite often.

00:00:25: Okay welcome to our AboutRogic podcast so I'm very happy Neil Ghani as a guest.

00:00:36: So Neil is now working for company, startup on AI and related.

00:00:46: if you can say more about it.

00:00:50: my start question was like Years ago, maybe twenty-five years ago Neil and I we worked together.

00:01:02: We worked out the theory of containers And using this used category theory in types theory to understand what data types and generic operations on data types?

00:01:16: Now Neil is still using category theory but To use it for AI which was interesting.

00:01:22: Maybe you can tell us a bit more about this.

00:01:26: Sure, well first of all I'd like to thank both you for inviting me.

00:01:29: It's a great pleasure especially because as Torsten said... ...I've known Torsten a long time!

00:01:35: We did our PhDs together in the nineties at Edinburgh and then we were both at Nottingham Together where we developed this theory of containers And Torsten has always been a source of inspiration.

00:01:48: his views on mathematics, especially on different formalisms and foundations.

00:01:53: And what they're useful for... Some of them are not so useful to other things.

00:01:57: All these things have always been a pleasure to listen to Torsten.

00:02:02: As Torsten says we invented those things called containers.

00:02:05: We just wanted some data type theory.

00:02:08: It's one of the really weird things that you read about where people say well You never quite know Where science goes you know, and they talk about all sorts of examples where someone invented something.

00:02:21: And then twenty years later it was the pivotal thing that unlocked something completely different!

00:02:26: It's often used as a way to really justify theoretical blue sky research because ideas are fundamental if their good will keep re-cropping up.

00:02:36: That is essentially what happened with containers When we did containers kind of like shapes and positions, so I could shape as a constructor.

00:02:48: And you've got holes where you put data in.

00:02:50: those are the positions?

00:02:52: It just dawned on me one day that well actually if you think about AI agents... ...and that's what the company I co-founded which is called CodemiTas and hopefully it'll allow me few minutes to plug it at some point we do a Gentik AI.. Well What Do AI Agents

00:03:09: Do?,

00:03:09: they need to respond to prompts.

00:03:12: So you've got a I wouldn't say a set.

00:03:14: I'd see it type of prompts And for every prompt, do you've gotta type with potential responses?

00:03:20: Oh my god That's the container.

00:03:22: and then they're really amazing thing is all The stuff we've done tossed an idea didn't end.

00:03:27: people like David Spivak have taken over Taken up on polynomial functors All this huge amount to work that has been done.

00:03:35: It's totally applicable too.

00:03:37: agentic AI in.

00:03:38: A really nice Thing Is that You know, ninety-nine percent of the world is using a sort of untyped version of GenTik AI.

00:03:47: Now all your listeners being into logic will understand the value types.

00:03:52: but for reasons I don't know The rest of the World has chosen to ditch To avoid...to go around this most amazingly useful and simple technology.

00:04:05: And our job at Kodomai is to replace current untyped agentiKI with typed agentiKAI and containers are technological scaffolding for doing that.

00:04:16: So it's interesting, maybe very knifely what the main without trying to do a netwith has been?

00:04:23: What other main benefits does like security?

00:04:25: because I mean lot of jailbreaking works with fluffy boundaries between inputs.

00:04:32: Well, I think the best way to explain this is just go back into very basic fundamentals.

00:04:39: In software development originally there were no types talking about going back in the sixties and seventies.

00:04:46: And then types came along.

00:04:47: they were amazing.

00:04:48: useful because you could find errors before running cause problems.

00:04:53: So a famous example was Apple plus five.

00:04:55: It doesn't type check Because Plus requires two integers.

00:04:58: Apple's a string not gonna work.

00:05:01: So the first use of these types was for type checkers to locate errors.

00:05:07: But actually, types have many other uses.

00:05:11: so they also give you if you like their formal logical presentation or specification.

00:05:17: what should your program do?

00:05:18: We'll write it down on a piece of paper very nice but pieces of paper with natural language at least until LLMs where not much can be done except read them.

00:05:31: So what you can do is, you can reflect the specification in a type.

00:05:34: And now it's mathematical object and code is a mathematical object so that the type-checker can check the code meets its specifications.

00:05:41: then gives your trustworthiness.

00:05:43: That's second thing.

00:05:45: But it goes on.

00:05:46: Types also allow scalability.

00:05:49: You cannot write big pieces of code from scratch.

00:05:51: You glue together bits of code already written.

00:05:55: But to check that this is possible, you really need to run through the whole codebase... ...to check each codebase doesn't adversely affect each other.

00:06:02: In theory!

00:06:03: That's time-consuming lots of resources.

00:06:06: quite error prone but with types The principle is you needed only checked at a type smudge not the whole Codebases.

00:06:13: so it's a principle of scalability.

00:06:16: And then there's, of course when you write to software system.

00:06:19: times change the operating requirements change and You need to adapt your system.

00:06:23: So you need to take a component out and put in new components.

00:06:27: same problem arises.

00:06:28: Are they unforeseen interactions?

00:06:30: Well if you get the types to match that is all you need To do.

00:06:34: so Types have become this amazingly useful and ubiquitous.

00:06:40: some people even don't notice them.

00:06:41: technology All codemies doing saying see those advantages.

00:06:46: Wouldn't it be nice if they could apply to AI agents?

00:06:50: Error checking via type-checking and ideally at compile time.

00:06:56: Trustworthiness, scalability adaptability governance harnesses you know You just go on an all the problems of a genetic AI that are not specifically about the LLMs That were at the core but about general software development at scale.

00:07:13: all advantages of types, we could have for a genetic AI.

00:07:17: If only you had to typed a genetic Ai.

00:07:20: that's what we've got.

00:07:22: So just one thing.

00:07:24: so you see it?

00:07:24: It's not about the actually is the LLMs But it's about the plumbing Which which are dry.

00:07:32: so your note You're not trying to use category theory to understand how lrms work.

00:07:39: Yeah yeah, so personally I'm NOT.

00:07:42: I mean there are some people in our team who are, and i'm interested.

00:07:47: And of course there's a lot of nice category theory about you know probability and vector spaces and the compact closed structure...and all sorts of big words.

00:07:58: so i'm interesting when we're doing that.

00:08:00: but fundamentally a gentek AI says okay LLMs like internal combustion engines.

00:08:05: they're an amazing technology!

00:08:07: You know?

00:08:07: But don't get from A to B. what you need is a car And that's what the AI agents community is about.

00:08:12: So if you like, it's everything after the LLM... ...that allows you to run organisations and do various things with agentic AI?

00:08:21: That's a part we do!

00:08:22: Having said that because we're typed Agentic AI in the middle of it will have an LLm.. ..and these LLms are typically untyped.

00:08:31: I mean Claude has a type It's called string arrow-string You know?

00:08:37: It's very

00:08:38: unstructured, right.

00:08:39: I mean it doesn't even use trees.

00:08:40: that uses sequences

00:08:47: in the phase... So we've got this typed preference framework and we have these untyped LLMs in the middle.

00:08:55: so how do you build typed LLMS if you like?

00:09:00: And fundamentally there are two approaches where investigating both of them.

00:09:05: One is a political metaphor.

00:09:09: Imagine an unstable area of the world, you know?

00:09:13: You could do nation building...you can go inside and try to make it well governed.

00:09:17: so that means going into the LLM's trying to produce structured output and take structured input.

00:09:23: That would be nice!

00:09:25: That one approach involves getting in to LLm technology.

00:09:28: there are people who work for us But the other one is just to have strong borders, if you like.

00:09:35: So we might have passport controls or something like that for customs.

00:09:39: so when the LLM produces some untyped outputs You then write a template and make sure this output conforms with that template.

00:09:47: This is seeping into the agentiKI community.

00:09:50: They usually use JSON but fundamentally it's an ascent type checking of the output To match expected input.

00:09:59: Sorry, type checking.

00:10:01: It's a nascent type-checking of the LLM output to make sure it matches what the system is expecting.

00:10:07: One thing which puzzles me about this The typical things about LLMs and machine learning Is that structure is emergent?

00:10:16: It's not sort of built in And category theory or types theory seems to be the other way around.

00:10:22: We have structure and we impose it.

00:10:25: How does this fit?

00:10:27: Well Good applied mathematicians understand that in the space between theory and reality, there's more theory.

00:10:40: So so The example I gave you was...the second version was accept where LLMs are And try to parse output of the LLMs To make it have a structure we want.

00:10:52: On other hand i also know branch research Where typing judgement is is usually boolean.

00:11:01: This term has this type or does not have that type, there are some small variants but fundamentally thats the case.

00:11:07: But maybe you can do probabilistic typing judgements.

00:11:12: I wonder if it's a cat?

00:11:16: Or is it a mammal?

00:11:17: Is it car-type?

00:11:20: and so on.

00:11:22: Essentially what we've got in vector space is probability distribution inside LLMs have that kind of probabilistic vector space-based type theory.

00:11:32: So maybe if it's not too far away from the more concrete, you mentioned now applied mindset would do this and then... And we had a few category theorists as guests.

00:11:44: so for was more narrative categories abstract nonsense always more theory.

00:11:50: I'm

00:11:52: going to say that is not abstract nonsense.

00:11:54: i am sorry

00:11:59: There is an application, but I mean there's a... It was

00:12:01: the joke by Grotendieg.

00:12:04: But people who don't understand this have say these things and if it has one thing i'd like to do is dispel that.

00:12:12: category theory Is The Way To Understand The World.

00:12:16: In My Opinion Of course its just my opinion.

00:12:19: everyone else can have their own opinion.

00:12:20: Yes The world Has Patterns And We Need To Find Those Out And category theory is just an amazing way of finding those patterns out, because category theory's a theory or structure.

00:12:30: You know?

00:12:31: There is debate!

00:12:32: Maybe the world is random and we have stochastic kind of fields like random fluctuations in this sort-of... ...way.

00:12:42: I don't think that's the case.

00:12:43: there are two thousand years of science to say it isn't The Case.

00:12:46: Some people believe It Is The Case but if We Accept That There Is Structure And even the probabilistic systems or the stochastic system, those have meta-theoretic structure.

00:12:56: So category theory is a canonical way to address that.

00:13:01: and thats what happened in programming language semantics.

00:13:02: we wanted to study programming languages.

00:13:05: We could've studied Java then we would of studied C a way to understand the design patterns within these languages, but at the LFCS where Torsten and I were doing our PhDs they came up with another better idea.

00:13:21: Let's study the meta-language of

00:13:23: programming.".

00:13:24: Of course that is what category three was really useful for because it was programing language independent.

00:13:29: so ML was developed.

00:13:31: this is ML or thirty years ago?

00:13:33: Not machine learning... Not

00:13:35: machine.

00:13:38: I remember when ML stopped being ML and became the new ML.

00:13:43: Okay, yes

00:13:44: same with logic right.

00:13:46: so yeah.

00:13:46: So in my career i've always loved category theory because it really makes things simple again for me

00:13:54: okay?

00:13:54: Yes

00:13:55: And um and I remember one I used to teach At universities and had students And, you know... You present something which they seem as a bit abstract and complicated.

00:14:10: They say oh god why are you doing that?

00:14:11: Why telling us all this stuff!

00:14:13: The art of teaching for me was always to get them to understand.

00:14:16: This is actually the simplest way to do it.

00:14:18: If we try another way there's complex problem Making many, many worse decisions and making more complex structures than you need to or you'd fundamentally reinvent the wheel.

00:14:29: And whether it's category theory Or any other form of mathematics that's a litmus test doesn't make your life easier.

00:14:35: So...and I think Category Theory does and i think The only reason people see Category theory as being abstract is they compare It To where They come from.

00:14:44: You know.

00:14:45: so if you Know linear algebra yes Category theories Seems Very Abstracted.

00:14:49: If You Know topology Maybe Category Theory Looks very Very sophisticated.

00:14:53: But if you're a topologist or do linear algebra to someone who does something more concrete, these will look really abstract.

00:14:59: and why we need topology?

00:15:01: I mean what's all this opens about some kind of metric spaces.

00:15:05: so i think it is just the question that people are familiar with.

00:15:09: By the way...I was teaching category theory also in the middle-end graduate school.

00:15:14: And uh..I was saying with category theory have two options You can either learn it or reinvented.

00:15:21: Yes, that's what I'm saying.

00:15:24: And it is tremendously useful.

00:15:26: and then we've talked about structure.

00:15:30: but the other connection with computation goes through type theory.

00:15:33: you know when i started doing logic in type theory these introduction eliminationals where do they come from?

00:15:42: You know various answers.

00:15:44: oh its the harmony of logic.

00:15:47: to someone like me I don't understand what that means.

00:15:51: Category theory, these are the universal properties... ...that define your type constructors of your logic.

00:15:59: So you know.

00:16:01: so That's computation!

00:16:03: There is this deep connection between category theory and Universal Properties And Type Theory and Introduction to Elimination & Computation And other foundations for mathematics.

00:16:11: Don't really have that?

00:16:13: Yes i mean types in technicality fit perfectly together.

00:16:18: You shouldn't really do one without the other.

00:16:20: We can't really go on with that, Mike.

00:16:25: But still I'm not... Maybe it's very useful to structure things but i wonder where this structure comes from?

00:16:42: of Platonism.

00:16:45: Is the world of ideas there first?

00:16:47: And what we see is a reflection on the World of Ideas, or maybe it's the other way around right?

00:16:54: so the word is just there and our mind in our culture and cultural evolution generates.

00:17:00: structures generate more better ways to understand structure.

00:17:07: So, I'm going to answer that by not answering that.

00:17:10: It feels like to me like, Torsten do you believe in free will?

00:17:14: Or maybe you should ask me Neil Do You Believe In Free Will?

00:17:16: it's a deep philosophical question...it is the reasonable thing To Ask Me.

00:17:20: What i would say Is..I don't know if we live on a Platonist at university.

00:17:28: The structure exists or Not.

00:17:30: However!

00:17:30: I do Know One Thing I Perceive That I Have Free Will And that's all it matters to me.

00:17:36: Absolutely,

00:17:36: I'm a pragmatic person so the category theory helps Me.

00:17:40: i don't know whether It's A sort of Imposition Upon A world Which isn't really Structured and Logical in Categorical In type Theoretic although this is since This Is a logic Podcaster i guess we all believe There some utility in Logic.

00:17:52: Maybe it Isn't imposition maybe the World isn't logical but We get a lot out Of it.

00:17:57: i mean another good example is atoms.

00:17:59: Atoms Don't exist you know, as in the kind of little solar system with a little planets sort of wandering around them.

00:18:06: But still it's useful explanatory tool allows us to do chemistry and sort of masses or stuff.

00:18:10: so even if I concede that um...you know The world is not categorical logical and type theoretic.

00:18:18: It's still very useful approximation.

00:18:20: That just my experience.

00:18:22: Yes but okay here when i was an undergraduate Yeah, it was in the eighties.

00:18:35: I was very fascinated by AI and this was what we now call Go-Fi is a good old fashioned AI right?

00:18:42: And this was structure based.

00:18:43: yeah It wasn't like... We use grammars, we used logical formalisms and we use them to model real systems.

00:18:53: There were lots of money pumped into this.

00:18:56: there was fifth generation computing.

00:18:59: It was a complete and utter failure.

00:19:02: And then why?

00:19:03: Because it was based on this idea, basically of I would say Wittgenstein the early Wittkenstein logical positivism.

00:19:14: everything can be reduced to logic... ...and that didn't work!

00:19:19: Then later new AI, these LLMs.

00:19:24: they were not based in paradigm Namely, they were not based on the paradigm.

00:19:31: You put in structure and then everything works.

00:19:34: but that structure as I said previously is emergent.

00:19:38: And it seems to me That category theory for example and type theory They are better.

00:19:46: The fit better with this go-for a picture because there very good in explaining structure.

00:19:55: But what do i wonder?

00:19:56: What you're doing?

00:19:58: Do they really fit so well with the new picture?

00:20:00: I remember

00:20:03: several points to make.

00:20:05: Firstly, there is more to life than LLM's Torsten.

00:20:09: So agentic AI has all sorts of things built on top of AI that interact and people want a reason about these systems.

00:20:16: They want trustworthiness, scalability, adaptability Catch me theory as meta languages are applicable for reasoning etc.

00:20:28: Now, someone might disagree with me.

00:20:29: They might say well eventually we'll just have this super powerful LLMs and everything

00:20:33: that you've got there.

00:20:34: Yeah

00:20:35: yeah.

00:20:36: so I can't say it's not the case maybe but at the moment There is no way that LLM.

00:20:45: So people who are trying to build essentially agentic AI using a kind of one big LLm strategy.

00:20:51: It doesn't work.

00:20:52: they're retreated from that LLMs in different places doing lots of different things.

00:20:58: Okay, how do you connect them?

00:21:00: Well You know...you could have an LLM in the middle trying to connect them.

00:21:04: but fundamentally The interactions aren't necessarily stochastic.

00:21:09: They can be well-deterministic they could be amenable to categorical and logical thought.

00:21:13: And that's what When I say it could be.

00:21:16: That is obviously a case that it is.

00:21:18: and thats what Code Am I Is Doing.

00:21:20: and all our success was built upon using good old fashioned type theory types, logic category theory to mediate that.

00:21:29: The second point is but if you go inside the LLMs as I said LLM's are a five year old technology.

00:21:36: so i agree with

00:21:37: your... But they're emergent right?

00:21:38: They're chain-seek?

00:21:40: Yeah yeah!

00:21:41: I agree with their analysis from the nineteen eighties.

00:21:42: it's possible people get overconfident in their technologies.

00:21:47: certainly your exam from the ninety eighties was one of them.

00:21:51: They say, oh look, LLMs did that.

00:21:53: That was amazing!

00:21:54: We can use LLM's to do everything.

00:21:57: but it might be.

00:21:58: actually when we looked back in ten years time... ...that kind of stochastic approach raced ahead through these amazing advances.

00:22:09: But later on, the logic started feeding back into organizing the internal structure of alinems and people working on this.

00:22:15: And that's what Neurosymbolic AI is.

00:22:18: It's an attempt to synthesize the best of stochastic in the best logical worlds.

00:22:23: So I can't give you a concrete answer.

00:22:26: The case has been worked out but there are lots who do not believe or accept the thesis That everything will be stochastical.

00:22:35: because if we did then why are all three here today?

00:22:39: Unless you have a secret fear that we are going to be made redundant.

00:22:46: To me, LLMs actually is the saviour of logic in a way especially our formal verification because like ten years ago I mean... We built these systems with rock or what's called cock or Akta and lean But actually there was this vision of formal verification.

00:23:14: Yeah, but the vision was not realistic because okay we could maybe verify a prime number generator yeah?

00:23:22: But any realistic piece or software Was out-of-reach.

00:23:25: Because oh The overhead here

00:23:29: and that's

00:23:29: not the case anymore I mean to me is the absolute saviour Of formal verification because you can But be careful.

00:23:39: No, but the point is we don't have to understand the LLM or whatever it's or the genetic framework.

00:23:47: We don't need to understand that as long its output produces something you can check which produces the evidence.

00:23:55: Okay

00:23:57: so It needs to be checked and typed.

00:24:00: If you're going to hand it the type checker needs be typed.

00:24:02: But that's exactly what Code of Mind does, is doing typed agentic AI.

00:24:06: so the agentic system is typed and hence they can be handed off to a typechecker.

00:24:09: So I absolutely share your opinion in fact The company co-founders based on that.

00:24:15: but remember your argument That you just made.

00:24:18: It wasn't... You didn't argue that LLMs Can't do everything?

00:24:22: No!

00:24:22: You said LLMS are great because They could take the burden a formal verification community.

00:24:32: Actually, our previous guest was the CEO of

00:24:41: harmonic AI.

00:24:45: And

00:24:48: they first were actually interested in type theory or anything but wanted to produce proofs and then produced proofs in English That there was no way for anybody to make sure that this was actually a proof and not just gobbledygog.

00:25:06: So then they learned Lean, produced Lean code which can be checked.

00:25:14: Yeah I know Harmonic Axiom is another company that's essentially there And fundamentally we're in that space as well.

00:25:20: We want to take our agentic systems and other systems to verify them, what differs from ourselves in those companies is they will just produce untyped stuff.

00:25:35: And then try and turn that untyped thing there trying to understand into a type thing the Typechecker can handle whereas we are making the agentic system itself typed.

00:25:49: so it becomes this sort of seam between the typed agentic is cleaner.

00:25:56: It's a fundamentally the same thing.

00:25:58: and inside agentic AI if you look at it, its fundamentally the structure as a Theorem Prover.

00:26:03: so not like your applying some technology to another one And they have completely different ones.

00:26:08: there are actually the same things.

00:26:10: I think this kind of Curry-Howard corresponded with theorem proving an agentic Ai.

00:26:15: Yeah well all i can say that even with the sort of unstructured approach these other names are pretty good producing type code even though they're not typed inside, right?

00:26:30: So to me I mean the problem with AI is trustworthiness.

00:26:37: And and i don't actually care how the internal work internally works as long as it can be produced some evidence that what it says.

00:26:52: For me, I mean the really positive aspect of modern AI is that it makes formal verification feasible.

00:27:04: Because you can certainly for really complicated, in a moment look more mathematical constructions where You would need to burn one or two PhD students, but you just give it your LLM and the LLm produces a proof.

00:27:29: It may make some mistakes... ...but then after iteration they will do that.

00:27:34: So doesn't matter for me if the LM itself is untyped, unstructured as my brain actually?

00:27:43: I mean my brain is untyped and unstructured i think!

00:27:47: So I'll

00:27:49: just say that Torsten, I hear you and have agreed with you three times.

00:27:51: And if you want to tell me we're getting formal verification is much easier because lean can

00:27:58: etc.,

00:27:58: et cetera in harmony can actually what they do?

00:28:01: I totally agree.

00:28:02: but i'm trying explain.

00:28:04: while I agree there are other advantages of types.

00:28:12: so for example how would we build large agentic systems?

00:28:16: Well, if you can type the components then we can glue them together at their interfaces.

00:28:20: And that's what Codemy does.

00:28:22: We're doing scalability of agentic error systems and we have components... ...and because they are types it can be glued together.

00:28:29: That is a standard thing.

00:28:32: The proof-is in the pudding!

00:28:34: You know?

00:28:35: We've got customers.. ..we're building large systems….

00:28:38: …the typed system is core to the scalability argument.

00:28:42: Can we maybe get into that?

00:28:44: Like, I mean if i'm very knifely.

00:28:46: I could Get my LLM and

00:28:47: say

00:28:48: here is the format please keep it in that format.

00:28:51: And so It's well tagged but of course That will not work all The time.

00:28:55: So how Is it?

00:28:56: is it like?

00:28:58: Let's build In and then there is another check on top Of it Maybe by other LLMs or How can I imagine to the guarantee that this output Is it on a time, or is the type?

00:29:10: Or maybe more like a bracket.

00:29:12: The output at whatever it is but my bracket guarantees its PDF because I put .pdf over simplifying.

00:29:23: So we have an agentic type system.

00:29:25: so here's the sort of thing you can do.

00:29:29: When i was quite young and learned functional programming And that was very nice one of the nice things Was i heard about this thing called functions as first-class citizens.

00:29:37: And then when I understood that, oh well it's quite powerful.

00:29:40: It means a function can take a function as input and return something... ...and there are plenty of patterns in functional programming to follow that great!

00:29:48: Now why is that?

00:29:49: Because on the logical side you have these Function Types.

00:29:52: On the categorical side we've got Cartesian Clothes and Monoidal Clothes Categories.

00:29:57: So We've developed that for agentic types.

00:30:00: so now our Agents Can Take Other Agents That Input Them And Produce Other Agences Output.

00:30:07: So our ages become first-class citizens and the only way we can do that is, We have a type system for agents.

00:30:12: Here's a concrete example.

00:30:14: Imagine you've got a sort of supervisor agent That has a lot of Concrete little Agents doing lots of Little things And Supervisor Agent Has to change that.

00:30:24: Change The behavior Of the Concrete Little Agents.

00:30:26: Either The Operating Environment Is Changed Or One Agent Isn't Really Doing Its Job Properly or Whatever.

00:30:32: Now If You Live In An Untyped World all these agents are fundamentally workflows.

00:30:38: And so the supervised agent is just a workflow, okay?

00:30:42: But really what its job to do?

00:30:44: it's?

00:30:44: take an agent which has a work flow and build new agent or transformed agent.

00:30:49: So there must be a Workflow Transformer but can't because of no type system.

00:30:54: Once you have this higher types then theres concrete dividend that you could have.

00:31:01: Can you have agent transformers as agents?

00:31:03: The type system gives you more and more powerful agents.

00:31:06: I would explain it this way to some people, imagine all you ever saw was real numbers because you live in an untyped world.

00:31:11: then the only type is real numbers.

00:31:13: And suddenly i say well imagine functions on a real number of transformers.

00:31:18: We call them functions.

00:31:19: they're incredibly useful and that's what we are doing with agents.

00:31:26: It's got higher order agents.

00:31:27: We call them meta-agents, they take agents as input through turn agents and we have a much greater explanatory power.

00:31:35: Well I realized this...I became very happy because most of my life And i think some theorists have a chip on the shoulder about it..we had this worry that were playing catch up with the bright hackers who just go off to do something amazing.

00:31:53: What you've done is this, well that's nice it clarifies things etc.

00:31:59: But there was a chip on the shoulder.

00:32:00: couldn't we have invented at first?

00:32:03: I always thought one area doesn't happen in particle physics.

00:32:07: It's fantastic!

00:32:08: The theorists are usually twenty years ahead.

00:32:10: They invent these ideas and then twenty thirty forty years later someone verifies them.

00:32:15: they're true

00:32:16: Sometimes not

00:32:18: Super symmetry, I mean

00:32:19: super symmetry was mathematically very beautiful.

00:32:24: But sometimes you know and of course we suppose it's a good example...I mean in the similar vein.

00:32:28: Einstein's relativity of course is good!

00:32:30: It took twenty or thirty years until it was validated by experimental observation.

00:32:40: And so what I've just given you is a little situation in agentic AI, where knowing the abstract mathematics being the theorist allowed us to do something natural which gives it something more powerful.

00:32:50: that's ahead of the game.

00:32:52: Now course everyone will catch up and its not as profound as any those other examples but It shows you that The ideas we developed over the last forty years Of software development programming languages type theory category theory are extremely valuable for a genetic AI.

00:33:11: And our amazing observation is people aren't using them, so that's why Code of My exists because we can use them.

00:33:19: So that's where I co-founded the company.

00:33:21: It is exactly to say you know types are good for agents not just with trustworthiness that Torsten was talking about but also for scalability and adaptability governance auditability logging all things you need do.

00:33:36: it can be governed in the type system.

00:33:40: Is there something on that part, which you would really like to stress now?

00:33:44: Otherwise I'd ask about a comment we made slightly before the recording.

00:33:49: We can also stick with

00:33:50: the coding.

00:33:52: I think I've said my piece fundamentally.

00:33:56: Types are good and you all agree with it.

00:33:58: Type have many applications not just trustworthiness.

00:34:03: People in agentiqi aren't using types, and therefore they don't have these advantages.

00:34:07: If only we could invent a type system for agents... It's not trivial!

00:34:11: You know?

00:34:13: it's just Martin left-type thing to write out your agentiqa and Martin left type theory.

00:34:17: But once you've

00:34:21: done that

00:34:22: We'll use containers And containers are of course our dependent types.

00:34:25: A container is a dependent type.

00:34:27: The power of containers does not the containers themselves, it's just to depend on type... ...the power of containers are the container morphisms.

00:34:34: for those who like a bit of mathematics If you have normal model of dependent types You call it FAM-set or FAMC as an example Whereas containers are FAM set up.

00:34:46: So there's a bit contravariance.

00:34:48: that happens.

00:34:50: That's a sophistication.

00:34:52: Why would we do that?

00:34:54: It doesn't look natural, I mean set up is an odd category but it has amazing properties both mathematically and in terms of applications.

00:35:03: Actually.

00:35:04: so there's one question which maybe just you talk a lot about types But actually where are the categories now?

00:35:13: Well Where do types come from Thorsten?

00:35:15: I think

00:35:17: of

00:35:20: this, category theory is a design space for types and that's exactly what we've done with Kodemi.

00:35:25: We wanted types for agents but weren't sure if they were.

00:35:27: It was not Martin of type-theory you know it wasn't Haskell or any of those.

00:35:34: What do we want?

00:35:35: And then he came up And the category theory explained it.

00:35:38: The category of containers has all this structure, and just like you know with Moji when he invented monads as not inventive monads but when he realized that monads represent a computational structure then Wadler took that into the programming languages.

00:35:51: we did exactly the same thing.

00:35:53: We've had this semantic domain.

00:35:55: It has these structures and all those structured terms compiles down in to a genetic programming language structure.

00:36:03: So was known?

00:36:05: Somewhere wasn't.

00:36:06: Actually, previously in this space we had Dana Scott and Dana once said that how lambda calculus should have been invented namely via Cartesian closed categories.

00:36:21: I mean it was not the way it was invented.

00:36:23: but here is due to Lumvec's observation... ...that this is how lambda-calculus i.e.

00:36:32: type theory should've been invented which just exactly what you're saying.

00:36:35: And when I went to Strathclyde and set up the mathematics structure program group, that's why we called it MSP.

00:36:42: because yes you can do programming but our thesis was a design pattern.

00:36:46: The patterns of programming are mathematical structure and that mathematical structure needs isolation.

00:36:52: and thats what the category theory is really good at.

00:36:54: so i think if just did type-theory would not have come out with our genetic system means step back into the category theorem find our categorical model And then it had all this structure.

00:37:04: That made a good and then we could...

00:37:07: It's an interesting design methodology, right?

00:37:10: Another weaker sense of structure.

00:37:11: but to go that direction is the principled way so you can think about development.

00:37:19: But I wanted to... Oh sorry!

00:37:20: Yeah New Fest.

00:37:22: Allright briefly then When we develop mathematical theories We often developed them in small scale because we're experimenting.

00:37:32: If they are Intricate and complex, on whatever at a small scale they're not really going to be tractable when we go the large-scale.

00:37:43: So you need our theories simple and beautiful.

00:37:45: And so that's nice space because the category theory forces us to do things universally in principle manner Not just write down random sets of brackets.

00:37:56: We only have ten concepts to use Ensign

00:38:03: coins, please.

00:38:05: Well that was in the blah blah blah.

00:38:11: I'm not sure if the random sets of brackets is a good pass to what i wanted to ask earlier.

00:38:17: we very shortly talk about foundations of mathematics and how the mathematical community's developing And even though it isn't your key area for work right now can invite you to speculate a little bit.

00:38:31: We'll category theory have more impact in the foundations of math, or should it?

00:38:39: So I think you're referring to a comment I made before we started recording.

00:38:43: And that was really about AI community going backwards.

00:38:46: and then going backwards is their rejection of types.

00:38:50: Okay!

00:38:50: That's what the AI community said.

00:38:52: okay now i got it.

00:38:53: sorry To

00:38:53: me the rejection of type is just...I don't understand It.. I mean Of course I've heard the arguments but to me they are not stuck up.

00:39:02: But we could talk about mathematics, it's quite interesting.

00:39:05: Torsten has talked a little bit about the impact of AI on mathematics.

00:39:09: I'm not one these people who are afraid...I think its brilliant Not just for reason.

00:39:16: Torsten mentioned We were in Edinburgh in the nineteen nineties when proof systems were being developed there and I remember Randy Pollock developing Lego.

00:39:26: Can you imagine there might come a day where, at conferences we expected all the mathematical theorems to be proven by a theorem prover.

00:39:34: And it's sort of bit of pipe dream.

00:39:36: but wouldn't have been nice to get that certainty and now within scope?

00:39:41: so... So thats amazing!

00:39:44: But theres other things that can happen.

00:39:48: when long time ago mathematics was about mathematicians It was about communication of ideas and explanations, an understanding.

00:39:58: And with the need for rigor came in the twentieth century... ...and this is not really my area at Torsum to know much more about it but all became about proofs.

00:40:07: that's a thing that counts!

00:40:09: With formal mathematics and formal theorem proves becomes about lambda terms.

00:40:13: So you're like Is This True?

00:40:15: Well here's my lambda term.

00:40:16: What do I do with the lambda term Apart from right through a type checker.

00:40:19: So I think that one of the things AI will allow us to do is focus more on Actually, what?

00:40:26: Do these?

00:40:27: What does it kind of social content off mathematics because they're doing their proofs?

00:40:33: More straightforward...I'm not gonna say straight forward but It becomes you know The difficulties less

00:40:38: visible.

00:40:39: yeah and he'll ask mathematicians To stop saying oh i'm just going to prove this theorem And asked them to think about where's valuable in what i'm doing.

00:40:47: And that's really important, and I would say to all your listeners if you sit down You're gonna try and do some work on something.

00:40:53: remember To ask yourself am i just plodding along?

00:40:56: You know is it interesting.

00:40:57: That I dot this eye across This tea?

00:40:59: what's really importan What's interesting whats valuable in what I'm doing?

00:41:03: and this Is true about how AI is going to affect not Just mathematics but or work low-level Work pen pushing I dotting T crossing.

00:41:12: AI systems will Do very well This will not displace humans.

00:41:16: Humans would be the ones who set the remits, who oversee actions and sign off on results.

00:41:22: And mathematicians... that's more fun!

00:41:25: That is better!

00:41:26: More interesting!

00:41:27: But do you mean

00:41:29: a bell?

00:41:30: I'm

00:41:31: just going to say mathematician will follow on in that direction.

00:41:34: And it'll be great for mathematicians because they'll be liberated, their creativity which is the essence of their humanity, Torsten you're shaking your head but creativity isn't important.

00:41:46: I agree!

00:41:46: But there's a common case of mathematical autism... Because mathematicians like Exactly not do what you suggest, namely to explain why they're doing this relevant and why it's useful or somebody should be interested in that.

00:42:08: I observed there are quite a number of mathematicians who start let X be whatever yeah?

00:42:15: And exactly focus on like dotting the eyes and crossing the T's and so on.

00:42:23: So is common defect, I would say of many mathematicians and what maybe attracts a certain personality to mathematics.

00:42:35: But i think you're saying that this particular type is actually something which we don't really need

00:42:53: anymore.

00:42:53: I mean, i think we have to understand that there are a lot of psychologies.

00:42:56: Of course and Certainly wrong of us to say certain psychological traits are good in certain psychological

00:43:02: No no

00:43:04: is the danger That you know he's sort of dismissed that kind of activity.

00:43:08: And of course mathematics is more prone To what?

00:43:11: You're talking about than say other demographics.

00:43:15: Yeah It's a fair point but I think that for the health of the subject it's really good to liberate ourselves from low-level eye dotting and T crossing, think about value in creativity.

00:43:27: Because that's where often good really insightful mathematics lies!

00:43:33: I mean just to defend myself.

00:43:34: i wasn't saying it was better or worse yeah?

00:43:39: I'm just saying this but... In the past these type of mathematics they would work on a proof is maybe not as useful anymore with the advent of reality, that's

00:43:56: all I'm saying.

00:43:57: Of course they will still be difficult proofs and it would more often happen in a case where the mathematician isn't replaced but have AI to help them guide your proof... Sure!

00:44:07: I don't think about myself being a full professor or run departments at grants or done mathematics ...I never consider my self good.

00:44:16: prover of theorems Exactly.

00:44:18: Some people are amazing, you know?

00:44:19: Can he prove this?

00:44:20: I don't know, it's complicated!

00:44:24: So those people who want to do proofs but should they explore this avenue or that avenue or the other avenue...I mean i just give up.

00:44:32: there is too much stuff But you can get AI assistance and help you DO your proofs.

00:44:37: so its not like doing proofs ever disappears And no one- I know YOU'RE NOT CLAIMING THAT AND I'M NOT Claiming That It's just a beneficial tool in my opinion.

00:44:48: I mean, just this comment.

00:44:51: Maybe one very impactful talk of Tao and the ICM about... This is a crisis not about a crisis of rigor but a crisis off their social structure because we use a lot of proxies right?

00:45:04: I'm near having paper used to show that

00:45:09: i am

00:45:10: capable of doing some math or it still does But in principle Does it really

00:45:17: show?

00:45:18: I mean, you know... So i would reject the word crisis.

00:45:21: I'd say its a golden opportunity!

00:45:23: I'm an optimist so some of you might disagree but im an optimists and think is a golden oppurtunity.

00:45:28: It liberates us from stuff that we used to have do humans aren't good at doing And so.. We should embrace this.

00:45:40: Its not a crisis.

00:45:41: Its an opportunity.

00:45:46: by fact, right?

00:45:49: You can have opinions.

00:45:51: And the papers you mentioned... I'm going to go back what i said about value and significance.

00:45:56: these are subjective.

00:45:59: some people might be uncomfortable with it but just like in art we often make decisions on what is better than others.

00:46:08: We like papers that that are more creative, and do interesting things in whatever.

00:46:13: So those papers you mentioned I think maybe we don't need so many of them... We all know there's a huge explosion of numbers published over the last fifty years And now they're just stuff published!

00:46:27: Do really need all these papers?

00:46:29: No one thinks it needs all this paper.

00:46:31: It is driven not even by mathematicians but university bureaucrats who want to measure stuff And they just weigh the papers.

00:46:39: That's not mathematics?

00:46:40: Yeah, I mean it will kill a lot of proxies and I mean proxie are proxys that aren't the real thing.

00:46:47: but this will make social structure change hopefully for better.

00:46:52: The only things where i really worry is learning because there was immense value in doing the messy detail work for awhile and then later what we get this weird?

00:47:05: You are now allowed to skip over the details.

00:47:08: Yeah, I worry too... I've seen a number of problems with AI and so apart from political social aspects or whatever it used be that if you didn't know the answer Now go to Claude and trot out some stuff.

00:47:26: he says And this is really bad.

00:47:29: I've seen a lot of senior people, you know they go around and do that kind of thing.

00:47:34: They trot out stuff...they don't know what their talking about.

00:47:37: This is really dangerous because it's going to mean the space for inquiry gets closed down Because people think they know the answer but they dont'know what they're talking.

00:47:47: abut That not good.

00:47:50: Another real problem is Claude from me.

00:47:54: i use alot of it.

00:47:54: I didn't think its fantastic.

00:47:55: It helps we do things But i know more than Claude.

00:47:58: To me, Claude is like a twenty-six year old precocious PhD student.

00:48:02: Yes works hard does lots of things talks crap quite often.

00:48:06: You know I mean I told Torsten recently or told Me that the category containers as locally cut easy and closed.

00:48:12: it's not.

00:48:14: And he gave you sketch proof?

00:48:15: And you know if you don't know more than Claude you just go.

00:48:18: oh That's fantastic brilliant.

00:48:19: i'm gonna write there in my papers now i'm going to build myself.

00:48:21: when we write my grants they use at all.

00:48:23: so And that's okay, because I know more than the precocious twenty-six year old.

00:48:28: But i see a lot of people just trotting out stuff they've got from Claude and They can't tell whether it is right or wrong.

00:48:34: This again you Know.

00:48:35: so People are going to...I worry That people not get The opportunity To grow into and learn all the skills Which makes them better Than Claude.

00:48:43: All their doing is Trotting Out Claude If they never do the proofs They'll Never know if Claud Proof Is True Or Not?

00:48:48: I mean I have Got this Very Concrete Problem.

00:48:51: I'm teaching a logic and how do you finish the logic?

00:48:54: And it's called, uh...I am using a proof assistant while I used COC when this was still COC.

00:48:59: Uh..and now i use Lean.

00:49:03: Now problem is that I set some exercises.

00:49:06: The exercises are formative really but have to evaluate them after assessing And previously, they would sit down and bang their head against this poof.

00:49:18: And while doing the poofs... Is that

00:49:20: allowed with health safety regulations?

00:49:23: Yeah exactly!

00:49:24: That's a problem.

00:49:26: The exit is there than everybody says

00:49:30: Yes but it was really good because you were stuck on something.

00:49:34: then worked around the lab to give some little hints.

00:49:38: They can just use an AI and the I will fill in the proof.

00:49:45: And that's too easy, and my analogy is going to tell them this It's like you go to the gym but say, I've brought this forklift with me and there is a forklifts.

00:50:01: I can lift all these weights very easily yeah?

00:50:05: But your muscles will not grow!

00:50:08: That actually

00:50:10: that it problem... And its manifested in people worrying about the senior say forty plus people.. Its'a great asset Earlier on in their career, it's dangerous.

00:50:24: And when the forty-first people are dead who is going to take that place because of skills they learned won't be learnt?

00:50:30: But what will eventually to some extent happen Is we'll adapt to AI We always do In education.

00:50:42: for all my life there has been a row back Of whats traditionally called liberal arts education Learning how think Its being replaced by skills based education.

00:50:51: can you do X, Can You Do Y?

00:50:53: Can YOU DO Z?

00:50:54: Now I think learning how to THINK is a much more important thing.

00:50:59: In the world where AI can do XY and Z we'll go back to.

00:51:03: CAN YOU THINK!

00:51:04: And so your class torsion...you will be asking them TO THINK ABOUT THE STUFF THAT CLAUDE IS DOING AND THINK ABOUT THE PROBLEMS AND COME UP WITH QUESTIONS AND THIS GOES BACK TO VALUE AND ALL THE OTHER THINGS THAT I WAS TALKING ABOUT.

00:51:16: So i see education changing for the better

00:51:20: Hopefully.

00:51:21: Epistemic

00:51:21: values can now rise again once the busy work is

00:51:25: solved,

00:51:27: yeah let's hope for that!

00:51:28: Yeah I mean it is.

00:51:30: you know as with all technology its dangerous in many ways but has no moral implicit value and how people use it.

00:51:38: some people used to be good or bad But in general, it is I believe the most transformative technology.

00:51:45: You know superseding The invention of computers and the invention on the internet because It will transform social relations in society In ways that we

00:51:53: do

00:51:54: indeed.

00:51:54: so So lots of good stuff.

00:51:58: And anyway when some people you don't like AI say Neil What are doing an AI?

00:52:02: A bad person Someone's going to try To make a good.

00:52:07: My excuse.

00:52:09: Actually, I mean even if technology is neutral you can nudge how it is framed right?

00:52:14: This area where we make a tutoring system that doesn't allow to just copy the answers.

00:52:21: Imagine

00:52:22: you could cut them off from the internet give.

00:52:30: This will also come back and oral exams, relics of the past with their own problems.

00:52:38: It'll be an interesting time at least for sure.

00:52:42: That sounds like one those Chinese proverbs you know?

00:52:44: Interesting in a negative way but I think it's...

00:52:51: Lovely!

00:52:52: Is there a topic that we forgot we should really talk about?

00:53:00: Listeners is if you know people who are looking for jobs Who have a grounding in software development AI type theory category theory functional programming?

00:53:14: Please get in touch with us.

00:53:15: We're expecting a large investment Any week now and so we definitely were hiring quite few people.

00:53:23: If you're an academic, can your instant collaborating with this as well maybe what grants any?

00:53:27: no You need.

00:53:29: You need industrial partners or maybe you just want to know what we're doing.

00:53:34: Get in touch with me, I'm sure that someone on the podcast talks and Dennis will leave my email address.

00:53:41: Yeah lovely!

00:53:42: We can add your e-mail not comment section but description of the video And people will find you.

00:53:50: Let's see if they are already in it.

00:53:52: Hey let me stress It is great that took time.

00:53:56: That was my pleasure.

00:53:57: talked about interesting

00:53:59: stuff.

00:54:00: Let me also stress to the audience, as always thank you for listening and commenting.

00:54:05: we try to reply too much possible.

00:54:08: in

00:54:08: particular thanks those who support us by becoming channel members or forwarding us to colleagues and friends sharing this video.

00:54:19: it's really a blast how positive energy we received.

00:54:24: so very thankful.

00:54:27: Anything more to say?

00:54:29: See you in a week for the

00:54:35: premises.