IngoBlechschmid

21 ms·

1. 181.▲
   by IngoBlechschmid 10y ago

   Tarsnap, online backups for the truly paranoid (mentioned on HN quite often): https://www.tarsnap.com/
2. 182.▲
   by IngoBlechschmid 10y ago

   Relevant short story by esteemed science fiction author Ted Chiang (author of /Story of Your Life/, which got turned into the movie /Arrival/): The Great Silence. http://supercommunity.e-flux.com/texts&#x
3. 183.▲
   by IngoBlechschmid 10y ago

   Sure, the Linux tool "pdftotext" works just fine for this. Two small caveats: ligatures get converted to proper Unicode ligatures and not their ASCII fallback (as one might want or expect) and of course complex mathematical formul
4. 184.▲
   Show HN: Experiments with randomness using client-side Python for children(speicherleck.de)

   1 points by IngoBlechschmid 10y ago|0 comments
5. 185.▲
   by IngoBlechschmid 10y ago

   I can't watch the video right now. But I can confirm that one can define what it means for a surreal number to be smaller than another surreal number in a meaningful way: So that the surreal numbers are totally ordered (for any two sur
6. 186.▲
   How Do You Fly to Alpha Centauri in Just 20 Years? Ride a Laser Beam (2016)(spectrum.ieee.org)

   2 points by IngoBlechschmid 10y ago|0 comments
7. 187.▲
   by IngoBlechschmid 10y ago

   Thank you for sharing that insight! Didn't know that.
8. 188.▲
   by IngoBlechschmid 10y ago

   That article is quite right regarding the take-home message to try to avoid inverting a matrix when other, more direct methods for solving the particular problem at hand exist. On page 2 of http://www.ti3.tuhh.de/paper/
9. 189.▲
   by IngoBlechschmid 10y ago

   "How else would you solve Ax = b for x, if not by computing the inverse of A (assuming A is a 3x3 or 4x4)?" For instance, there a fast iterative solvers. They start with an initial guess for the solution (which can be an arbitrary
10. 190.▲
    by IngoBlechschmid 11y ago

    Incidentally, this topic gave rise to a much larger theory, namely mirror symmetry (unrelated to reflection at everyday mirrors). Please take the following account of the history with some grain of salt, I'm not an expert on this top
11. 191.▲
    by IngoBlechschmid 11y ago

    I'd like to draw attention to a fact already pointed out by Chinjut in this thread: The original formulation of Euclid's proof is in fact entirely constructive, contrary to what the article claims. Michael Hardy and Catherine Wood
12. 192.▲
    by IngoBlechschmid 11y ago

    There a ways to formulate "the infinity of the prime numbers" without any recourse to a previously-constructed set of all prime numbers (or even all natural numbers). Two such ways are: 1. "For any natural number n, there is
13. 193.▲
    by IngoBlechschmid 11y ago

    The book is truly excellent. You need some knowledge of (partial) derivatives and matrices, but other than that it doesn't require any more sophisticated mathematics. We used it to prepare a 10-day course on neuronal networks for high
14. 194.▲
    by IngoBlechschmid 11y ago

    There is an experimental browser project which was created for this very reason (tree-like history): http://rainbow-lollipop.de/ (page is in English)
15. 195.▲
    by IngoBlechschmid 11y ago

    Sorry, didn't intend to use so much jargon. By "quantifying over all formulas" I just meant that one has to distinguish between the following two statements: 1. The law of excluded middle holds for a particular formula p. 2.
16. 196.▲
    by IngoBlechschmid 11y ago

    I didn't check it. If you want to do it (the key step being to verify that the axioms of intuitionistic logic holds for your definitions of AND and OR), you can check Wikipedia for the list of axioms to verify: https://en.wi
17. 197.▲
    by IngoBlechschmid 11y ago

    Your counterexample could work, but it is not obvious that it does so. This is because you also have to give definitions of ∧, v, and ==>, and then check that your definitions satisfy the axioms of intuitionistic logic. As stated, your e
18. 198.▲
    by IngoBlechschmid 11y ago

    You are right that for a particular formula p, the implication (~p ∨ p) ⇒ (¬¬p ⇔ p) is an intuitionistic tautology and that the reverse implication is not (in general). However the situation is different when you quantify over all formulas.
19. 199.▲
    by IngoBlechschmid 11y ago

    Your comment is a good first approximation to the motivation for HoTT! However, let me add a couple of remarks. Firstly, HoTT can also be used with classical logic, i.e. where you freely use the law of excluded middle. This does not impact