thoran

5 ms·

1. 1.▲
   by thoran 11y ago

   On the other hand, when you do have categories in a language and not the smartest people in the language's community, you do have real problems: You end up with conflicting definitions of homonymic methods because every one wants his
2. 2.▲
   by thoran 12y ago

   It's my fault, I think I read your answer too quickly and miss a negation somewhere. So, yes, a formal rewriting of Wiles' proof is "only" a practical challenge. But a big one. Just about 15 years ago, we were just abl
3. 3.▲
   by thoran 12y ago

   No, you're wrong. This is not a theoretical issue there, but a practical one. Almost all mathematics (and this certainly includes Wile's proof) could be written in Coq, in theory. It is extremely hard to do in practice. Mathemat
4. 4.▲
   by thoran 12y ago

   On MacOS, you would distribute a library as a 'Framework' (a package containing the binary shared object, headers, documentation, resources, sub frameworks...). In Xcode, you can quickly add a framework dependency. And if you ne