HNHacker News
TopNewBestAskShowJobs

SkidanovAlex

140 karma · joined June 27, 2012

submissionscomments
SkidanovAlex··on Formalizing Fermat's Last Theorem
It is the latter. If you are certain your theorem is stated correctly, and you believe that the Lean kernel against which you validate is correct, your proof is correct.

This is how the theorem for FLT looks in the particular proof we discuss here:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

As long as this statement is correct, and the kernel is correct, the proof could be trillion lines of code, and if the kernel says it is correct, it is correct.

This proof was checked against TWO independently built kernels. So you would need TWO kernels to have the same bug to mistakenly accept an incorrect proof.

(Not impossible: such a bug indeed was recently discovered (and patched))

SkidanovAlex··on Google removes "Doki Doki Literature Club" from Google Play
Given your description, it is very likely that you actually only completed the act 1 of the game. The "jump scare" is not the end.
SkidanovAlex··on Show HN: Term.everything – Run any GUI app in the terminal
Isn't the first example (with the cartoon) in text mode?
SkidanovAlex··on Stripe Launches L1 Blockchain: Tempo
The most important aspect of blockchain that is relevant here is that your counterparty half a world away and you both agree that you trust the state of this blockchain, and thus can transact on it.

For business running the same code on their 1 node instead of N is not a replacement, because their counterparty has no reason to trust whatever is running on that 1 node.

Your reasoning re: N nodes are expensive is also flawed. Executing a single payment transaction takes a fraction of a second of compute. Even if it is replicated 10,000X, it's still extremely cheap compute-wise. The low cost of transactions has nothing to do with subsidizing.

SkidanovAlex··on Windows XP Professional
MS Paint though is "either real or a Good Clone :)", because you can zoom to 12x by clicking one-pixel-wide line below 8x.
SkidanovAlex··on I Went to SQL Injection Court
While I believe that the city should share the schema, and that the city is effectively argues for security through obscurity, I disagree with the main premise of the article: that knowing SQL schema doesn't help the attacker.

If I understand the argument of the author here:

> Attackers like me use SQL injection attacks to recover SQL schemas. The schema is the product of an attack, not one of its predicates

The author appears to imply that once the vulnerability is found, the schema can be recovered anyway. It is not always the case. It is perfectly viable to find a SQL injection that would allow to fetch some data from the table that is being queried, but not from any other table, including `information_schema` or similar. If all the signal you get from the vunlerability is also "query failed" or "query succeeded, here's the data", knowing the schema makes it much easier to exploit.

> the problem is that every computer system connected to the Internet is being attacked every minute of every day

If you specifically log failed DB queries, than for all the possible injections that such 24/7 attacks would find you have already patched them. The log would then be not deafening until someone stumbles on the actual injection (that, for example, only exists for logged in users, and thus is not found by bots), in which case you have time to see it and patch before the attacker finds a way to actually utilize it.

Knowing schema both expedites their ability to take advantage of the vulnerability, but also increases their chances of probing the injection without triggering the query failure to begin with.

SkidanovAlex··on Tree Calculus
Would help a lot if somewhere at the very top it explained what tree calculus is (may be extend the animation of the addition example to first show what the t is)

It took me a while on the website to understand what it was all about. As it is it looks more like a website for a functional programming language.

SkidanovAlex··on Reconstructing images a person sees via non-invasive brain scans
There's an outstanding episode of Black Mirror called Crocodile, that explores this idea.
SkidanovAlex··on By Exploring Virtual Worlds, AI Learns in New Ways
USS Calister is also a very good episode with the same premise.
SkidanovAlex··on Do You Love Me? [video]
Watch Black Mirror episode called Metalhead.
SkidanovAlex··on YouTube to remove content that alleges widespread election fraud
Who decides that the videos in Russia are factual, while the videos in the US are not?
SkidanovAlex··on Nightshade: Near Protocol Sharding Design [pdf]
I'm the first author of the paper, happy to answer any questions
SkidanovAlex··on Why Go?
If anyone used both rust and go, are there any big advantages of go over rust (besides simplicity)?
SkidanovAlex··on Richard Stallman and Future of Software Innovation
Exactly.

Similarly, Google quality is in big part due to invaluable information of what URLs were clicked for what queries.

If duckduckgo had access to that information, their quality would've been way higher, and there's no reason I as a user shall not be able to give access to the information I generated for Google to another service.

SkidanovAlex··on For YC Companies Raising Seed Rounds
The advise I give to all the YC companies is: prepare for the investor day as much as you prepare to the demo day.

The investor day can save you a lot of time fundraising later if you close few people on the spot, so make sure to be ready for a 20 minutes session with a longer coherent pitch and answers to the common questions.

In my batch (W17) the investor say was completely deemphasized for some reason, and many companies came unprepared, myself included

SkidanovAlex··on Experts cracked laptop of crypto CEO who died with $137M, but the money was gone
Love the "into the ether" pun
SkidanovAlex··on What you need to know before you join a startup
Since there's no barrier to start a startup, there will always be companies at which the growth will be slow.

A good startup with strong engineering team and fast shipping cycle will provide with way more learning opportunities than FAANG.

Personally, I think for a fresh grad going to an early stage startup or to FAANG is a close call in terms of value. 1.5-2 years at FAANG gives a good boost to the resume to pursue better opportunities later, while 1.5-2 years at a startup can provide more learning and potentially some upside already. At that stage there's time to take chances either way. A close-to-IPO company is also a viable option.

My goal in the article was not to say startups are bad (or good), but rather to provide insights so that people can make more informed decisions.

SkidanovAlex··on What you need to know before you join a startup
While P(Russian|ICPC Winner) is high, P(ICPC Winner|Russian) is still pretty low :) Also, Illia is Ukrainian, not Russian, but it's nitpicking.

ICPC is a great way to start your career if you were unfortunate enough to get born in a noname city somewhere in ex-Soviet Union, thus people are pretty motivated to do well. In US by the time you graduate you already have few internships in your resume, and are pretty figured career wise, so naturally the benefits of ICPC are less attractive.

SkidanovAlex··on What you need to know before you join a startup
"unlikely to cover what you would have made if you joined Google instead." refers to what you would have made if you joined Google few years ago, not at its early days
SkidanovAlex··on List of hackathon tips. How we got $7250 bounties on ETHDenver
Congrats again on a stellar performance!

My 2 cents: back in a day when I was going to Angelhacks frequently, we would show up early and go through all the sponsor booths. The idea was to find a sponsor that is relatively small (and thus really cares about adoption) and that has a large prize ($1500+), and completely commit to building on them. Spend time at their booths, understand their API to the lowest level details, and build a hack that showcases their strengths.

Since most of the other teams usually just plug the sponsor APIs at the last moment, someone who was committed is more likely to win the prize.

I won this way $1500+ on 4 different occasions.

SkidanovAlex··on Ethereum: A number of hard forks turn out to be scams
You don't need to go to top 100. Two Bitcoin forks that are scams are in Top 10 right now.
SkidanovAlex··on Unsolved Problems in Blockchain Sharding
That is somewhat similar to what Vlad Zamfir's sharding is doing (https://medium.com/nearprotocol/so-what-exactly-is-vlads-sha...)

For a given transaction you'd only need to verify log(n) chains, but the problems from the top level post remain. The question is how you verify the transaction in a given chain. If you verify the entire chain, than you are expected to end up verifying all the chains (since ultimately cross shard transactions will be coming from all shards), removing any benefit from sharding. If you somehow trust that the shards were doing their job properly, then you need to somehow deal with shards being corrupted.

SkidanovAlex··on Unsolved Problems in Blockchain Sharding
Alex from Near is here, the author of the post. Would be happy to answer any questions.
SkidanovAlex··on How NoSQL forced the evolution of a scalable relational database
> To use SQL, even an in memory one, in such use case is not going to work.

Have an index on the score and select with ORDER BY ... LIMIT?

SkidanovAlex··on MemSQL (YC W11) Raises $36M Series C
As a matter of fact, MemSQL hasn't ignored them for a while now :) I think since 3.2.

But I don't think many customers are taking advantage of it though.

SkidanovAlex··on Asana Engineering Interview Guide
The very next sentence there is "Our goal is not to simulate day-to-day software development", so no, they probably do not unplug the internet connection for the existing programmers.
SkidanovAlex··on A Message to Our Customers
> People use them to store an incredible amount of personal information, from our private conversations to our photos, our music, our notes

I wonder if this is a grammar mistake, or Apple actually considers the private conversations, nodes, photos to be theirs?

SkidanovAlex··on Metabase: Why we picked Clojure
> (take 1000 (mapcat (fn [i] (repeat i (odd? i))) (range)))

And this example is suppoed to support Clojure's readability?

SkidanovAlex··on The 'risky bet' that saved Facebook hundreds of millions of dollars
> "Most companies are not Facebook or Google," Paroski says.

This is a very accurate statement, for as long as there are more than four companies.

SkidanovAlex··on MemSQL Launches Unlimited Community Edition
MemSQL partitions data across nodes by hash, not by range, so partition prunning is less applicable. However, in a case when it can be applied MemSQL does apply it. [1]

Within each node, for column store tables in MemSQL we do use segment elimination very aggressively, which is effectively the same thing as partition pruning. [2] [3]

[1] http://docs.memsql.com/latest/concepts/distributed_sql/#inde...

[2] http://docs.memsql.com/latest/concepts/columnar/#query-effic...

[3] http://docs.memsql.com/latest/concepts/columnar/#maintenance...

Page 1 of 2Next →