Hi! We finally released a paper describing our methodology for the proof assistant.
It's available on arXiv here: https://arxiv.org/abs/2009.03393 Any feedback/suggestions or questions is obviously welcome! Special shout out to David Wheeler and Mario Carneiro in the acknowledgements that I want to reiterate here: "" Finally, the authors would like to thank the whole Metamath community for their support, feedback, and encouragement, in particular, David A. Wheeler for his motivating enthusiasm and Mario Carneiro for his precious help on a wide variety of technical questions. "" Hope you enjoy it. -stan -- 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/CACZd_0wJLEBRrV4-KetA-uiEXo4mG3KKcoYQZqHjEnppz0%2B8SQ%40mail.gmail.com.
