Tweetovi
- Tweetovi, trenutna stranica.
- Tweetovi i odgovori
- Medijski sadržaj
Blokirali ste korisnika/cu @jix_
Jeste li sigurni da želite vidjeti te tweetove? Time nećete deblokirati korisnika/cu @jix_
-
Prikvačeni tweet
I'm super excited to announce a new result: sorting 11 inputs using a sorting network requires 35 comparisons and sorting 12 inputs requires 39 comparisons. I used a new search procedure w/ a formally verified checker, all on github: https://github.com/jix/sortnetopt 1/11
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
It caught my eye, as I really like Lakatos' "Proofs and Refutations" https://en.wikipedia.org/wiki/Proofs_and_Refutations … about how proofs and definitions change and get patched when counterexamples are discovered or views shift and how that is part of mathematical progress. All using Euler's Poly. F. as ex.
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
I love reading books about the historical development of various mathematical subjects. I really enjoyed and just finished reading Richeson's "Euler's Gem" https://press.princeton.edu/books/paperback/9780691154572/eulers-gem … which covers the birth of topology, starting from Euler's polyhedra formula (+ history of that).
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Jannis Harder proslijedio/la je Tweet
If you are looking to hire "truly exeptional engineers and product persons" (quote of an external contractor) with a strong math background, or want to hire me, let me know. Team and I suddenly find us in the weird position of having to find new work. We are free starting... now!
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Jannis Harder proslijedio/la je Tweet
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi
-
On my way back to Leipzig for the
#36c3, looking forward to seeing lots of awesome folks again :) Also if we haven't met and you want to change that, feel free to say hi!Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
The core idea is to start with the semantics of a programming language and using types to encode facts about programs instead of starting with a formal system. Now I really want to write my own toy language/proof assistant based on that but my overflowing pile of projects says no
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Somewhat unexpectedly youtube recommended a great lecture by robert harper about computational type theory: https://www.youtube.com/playlist?list=PL0DsGHMPLUWXXA8RHzVZ2B5E5hP8CD15Z … It's a different approach (vs formal type theory) that I haven't seen before and that makes some things less confusing.
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
A (German) talk on SAT solving I recently held is online now. Wish I had found more time to rehearse it, felt like a bumpy ride to me, but I got positive feedback anyway :)https://twitter.com/nookorga/status/1206136817445040128 …
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
The bound for 12 inputs follows directly due to an old result of Van Voorhis. Next I need to write up how and why all of this works. 11/11
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Still it reduces the amount of work required from the verified part a lot, so I could use naive, easy to verify code and data structures. Today I finally got to the point where my formally verified checker printed `Just (11,35)` :) 10/11
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Instead of directly checking the output of the search, I also introduced a post-processing stage that simplifies the output of the search and reduces it from ~100GB to ~3GB in size. Doing this during the search didn't work out. 9/11
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
The classic workaround here is to generate a certificate from the search and write a separate formally verified program to check that, in the hope that it'll be less work. That's also what I did. 8/11
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
To make sure my results were correct I wanted to formally verify my code. For formally verified code you usually have a performance/verification-effort trade-off. Compromising on the performance of the search wasn't an option though. 7/11
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Scaling this to 11 inputs was still a challenge. Storing the explored search graph, would take over 1TB of memory. By recomputing the edges on the fly I managed to get this down to ~200GB. Making use of multiple cores was also tricky. 6/11
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
While working on this, I came up with an idea that allows to prune even larger parts of the search space and do so with less computation. With this I can get the bounds for 9 and 10 inputs in 10 seconds on my laptop. 5/11
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Earlier this year I optimized that approach and got down to 2h on a 16-core machine https://github.com/jix/sortnetopt-gnp …. Experimenting with this made me realize that scaling this to 11 inputs would take way too much resources. 4/11
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
Finding the bounds for 9 and 10 inputs in 2014 took over a week on a 144 core cluster. In the meantime the approach used for that result was optimized to take 11h on a 32-core machine https://doi.org/10.1007/978-3-030-19212-9_19 … 3/11
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi -
These new lower bounds match the existing upper bounds, so we get two new terms of https://oeis.org/A003075 . The previous two terms were found in 2014 https://arxiv.org/abs/1405.5754 . The terms before that in 1966 by Floyd and Knuth. 2/11
Prikaži ovu nitHvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.