Well .. I didn’t reply to the mailing list because it contains some insulting words to third-party products. But since you forwarded it already, I’m fine with that.
I didn’t know you were looking for formalizations of pure mathematics theories, but here is my another little experience: 1. Go to "Formalizing 100 Theorems” web site [1] and find a theorem in your targeting area. 2. Choose one of the formalization under that theorem (if there is), based on the theorem prover you know how to use. 3. We can imagine the formalization of that theorem must depends or ships with a large piece (if not the whole) of underlying math theory. The only sad thing is, this web site didn’t mention any work done in HOL4 (and its predecessors). While the closest one is HOL light, of course. I think migrating theories to HOL4 from other theorem provers is not always straightforward but still doesn’t create much academic value, unless you can push the related theories to a higher level. Regards, Chun Tian [1] http://www.cs.ru.nl/~freek/100/ > Il giorno 10 set 2017, alle ore 21:31, Mario Castelán Castro > <marioxcc...@yandex.com> ha scritto: > >> Why did you ignore Google web search (www.google.com) and Google scholar >> search (scholar.google.com)? DuckDuckGo is built-in supported by some open >> source products, but I think it’s generally a garbage. > > Google has a lot of private data about people. They can do, and do, many > bad things with this data. I can not stop Google surveillance, but I do > not want to make their task easier. Anyway, Startpage is an independent > proxy for Google Search therefore the results should be similar to what > Google Search would provide directly. In my experience DuckDuckGo has > served well enough. It is my main search engine. > > Unfortunately, I still use Google Scholar because I have not found a > good general purpose alternative. I use PubMed when I need to search for > publications in medicine, but for mathematics/logic I do not know of any > good alternative. Suggestions would be very welcome. > >> My experience: “HOL4” is a bad key word, because mostly what you may found >> is a formalization done in old HOL versions. Instead, “formalization” + >> “higher order logic” + domain keywords should be enough. > > Thanks! This gives much better results for my aforementioned benchmark > test about prime numbers. ☺ > > There seems to be no signification formalization of elementary topology > in HOL4. I am aware that there is some topology in “/src/real” in the > HOl4 distribution, but it is very limited. Searching with DuckDuckGo, > Startpage and Google Scholar for “formalization "higher order logic" > topology” does not turn anything relevant. As my first development with > a proof assistant I am formalizing some theorems of elementary topology > in HOL4. I plan to develop and publish a theory which is suitable as the > foundation for further developments. > > If you know of an existing formalization of elementary topology in HOL4 > please let me know, so that I can avoid duplicating work. > > Regards. > > Note: It seems that you forgot to reply to the mailing list. > > On 10/09/17 13:34, Chun Tian (binghe) wrote: >> Hi, >> >> Why did you ignore Google web search (www.google.com) and Google scholar >> search (scholar.google.com)? DuckDuckGo is built-in supported by some open >> source products, but I think it’s generally a garbage. >> >> My experience: “HOL4” is a bad key word, because mostly what you may found >> is a formalization done in old HOL versions. Instead, “formalization” + >> “higher order logic” + domain keywords should be enough. >> >> Regards, >> >> Chun Tian > -- > Do not eat animals; respect them as you respect people. > https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan >
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
