> > > I left a comment under Hotz's video and invited him to visit this > thread. If we are lucky, we will see his ideas here. >
That sounds like a nice idea, it might be nice to reach out to him a bit more formally. I'd be willing to answer questions if he has them and I'm sure there's a bunch more people who know much more than me who would too. I think the reason he is doing this is this project he is doing. http://backspace.ai/ I agree that metamath is an awesome starting place for formal logic and so it would be cool if he got into it. There is a contact on that page and I imagine it's better if someone more important than me emails him though I am happy to if no one else is interested. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/44e843b0-daa1-404b-bf67-47865246bbdc%40googlegroups.com.
