Hacker News Reader

joycianon Learning How to Prove: From the Coq Proof Assistant to Textbook Style

Well, there is the Naproche-SAD project:

https://github.com/Naproche/Naproche-SAD/blob/master/README....

> Proof Checking of Natural Mathematical Documents, with optional support for Isabelle Prover IDE.

The goal is to be able to proofcheck from Latex directly. Most of the machinery is (used to be) written in Haskell. It is definitely a cool project, and they could definitely use help.

joycianon Facebook, WhatsApp Will Have to Share Messages With U.K.?

It's impressive, thanks for taking the time.

joycianon Facebook, WhatsApp Will Have to Share Messages With U.K.?

How do people post such comments? Do you have these lists of source links just saved somewhere or do you just do it on the spot?

joycianon Consciousness Doesn’t Depend on Language

I love how this immediately stumbles upon difficulties: this is a different 'chair' than I was thinking of and the first definition just invokes a recursion into the definition of 'conscious'. I'm not sure whether that was the purpose of the comment, but it brilliantly succeeded.

joycianon The Future of Mathematics? [pdf]

Aren't humans bounded in the same way? Why not build a system that's faster than us?

joycianon Halt the use of facial-recognition technology until it is regulated

I would like to seriously ask you to consider a more nuanced stance on this subject, as you now seem either uninformed about the technology behind these systems or wilfully naive. Please consider the dangers that could spring from such capabilities, if not now, then in some time when another power has control of these capabilities.

joycianon How close are we to 3D printing the human heart?

How many cells need to be regenerated for you to be a new person? The ship of Theseus is totally uninteresting to me and to be honest I think it has never been interesting. It's just calling attention to the fact that arbitrary definitions are arbitrary.

joycianon Are We Living in a Computer Simulation? Let’s Not Find Out

https://en.m.wikipedia.org/wiki/Superdeterminism

joycianon A Programmer’s Regret: Neglecting Math at University

Sounds very cool. Is there any way to follow your progress?

joycianon A Programmer’s Regret: Neglecting Math at University

Can you tell me more about your project to get lean working on the cloud providers?

joycianon A Programmer’s Regret: Neglecting Math at University

If it has been proven from your axioms (really down from the axioms!) then you can add it to a library of statements you 'know' (or in the case of your axioms, assume) to be true.

joycianon The case against reality

As soon as the article started mixing in the quantum mechanics quotes, my eyes glazed over and I stopped reading. Do people really get something out of these kinds of articles?

joycianon The case against reality

Definitely.

joycianon The case against reality

> Perception may not be reality

From a compression perspective, of course it is not ...how else would you model your environment?

Consciousness is just a glorified 'top' command. Our visual cortex has evolved over millions of years to distill our environment down into a much lower dimensional space.

Additionally, I would rather have them phrase it like neural activity creates consciousness (which in my opinion is almost a meaningless tautology).

joycianon Bedridden for 11 years, he discovered a surgery for his adrenal condition

Isn't sleep apnea more common in overweight people?

joycianon The Trouble with Many Worlds

Thanks for calling out how the Canon interpretations of QM do not not actually save us from much of the problems that are objected to in other interpretations. Sometimes I feel like everyone just repeats what they heard as a student. Smolin's work looks interesting, thanks for the recommendation.

joycianon The Trouble with Many Worlds

Realism can be salvaged in a fully deterministic theory.

Note however that empirical science in a deterministic world is a strange concept.

Edit: However in my opinion empirical science in a nonlocal or nondeterministic world is equally strange, if you really think about it.

joycianon A Quantum Theory That Peels Away the Mystery of Measurement

I would rather these kinds of articles just explain the uncertainty principle in a wave mechanics context, without any quantum theory to obfuscate.

Or else just go "What if AB != BA?" and actually somewhat give people an entrance point to what is actually happening.

joycianon What If Life Did Not Originate on Earth?

https://www.nature.com/news/force-of-nature-gave-life-its-as...

Nature might be slightly biased due to the asymmetry of the weak force.

joycianon What If Life Did Not Originate on Earth?

Why are there no other human species (anymore)? Because there was no room for them anymore and they could not compete. In the same way, it it very well possible that life utilizing other genetic code got stamped out (early on).

joycianon Word2vec: Fish + Music = Bass

The sparse tensor perspective intrigues me, could you perhaps provide me with some references?

joycianon Why Our Postwar “Long Peace” Is Fragile (2018)

As far as I can find, the military casualties of the (decade-long) Napoleonic wars were around 3 million.

The Crimean war caused close to 1 million casualties in 3 years.

https://en.m.wikipedia.org/wiki/Crimean_War

The war involved Second French Empire, British Empire, Russian Empire and the Ottoman Empire.

Perhaps there are other examples of major wars, but this one seems significant.

EDIT: Outside of Europe, consider the Taiping Rebellion, with the highest deaths estimates at 30 million (or even higher!). The British and French got involved as well.

https://en.m.wikipedia.org/wiki/Taiping_Rebellion

joycianon MIT: Building on Julia programming language to open up AI coding to novices

Julia's ecosystem is rapidly catching up with R and Python (and it already has interop with those languages). I am quite fond of the language and would not be averse to using it as a main language in the near future.

This seems like a welcome addition. The tutorials are clear.

joycianon Finland’s weekly news show in Latin cancelled after run of 30 years

Livy, Seneca, Cicero, Virgil also featured in my Latin classes. I'm not sure of the relative difficulty levels anymore, though. All of these were fascinating for different reasons: Livy for the narrative, Seneca for the wisdom (see also Montaigne who heavily quotes Seneca in his essays), Cicero for his personal involvement in Caesarian politics and Virgil for his role as Augustus' propagandist and continuation of the Homeric tradition.

I should read more of these texts, I remember being really fond of Latin classes.

Edit: to concur with GP, Caesar's writings (de bello Gallico) were somewhere in the first half of the curriculum and were definitely regarded as relatively easy.

joycianon Ask HN: How to get better at Data structures and Algorithm?

Read this book:

https://www.amazon.com/Introduction-Algorithms-3rd-MIT-Press...

It's all in there. Put away a week of time to really start digging into it, get into the habit of learning from a book. I'd say it's worth it.

joycianon Universal Logic Gates (2015)

This article shows more universal gates than the NAND and NOR that are usually discussed. Are any Hacker News users knowledgeable about the topic? Because I was wondering why I never heard about these universal gates before. Almost always, only NAND and NOR are discussed.

joycianon Do Brains Operate at a Tipping Point? New Clues and Complications

The theory makes little sense, see also Max Tegmark article on it.

joycianon An Infinitely Large Napkin

The fact that Z denotes the set of integers is a sort of mathwide standard. It comes up a lot (number theory, group theory) Did you major in some specific area of maths? Or is it just the span of years between?

joycianon Quantum Leaps, Long Assumed to Be Instantaneous, Take Time

I think it does call into question the power of science, but also: assuming non-determinism does not give us this power back! If materials (atoms / humans) can arbitrarily disregard the laws of nature by making choices (however that would be implemented), what does an experiment even mean?

Edit:

This is a relevant theorem, that nicely complements Bell:

https://en.m.wikipedia.org/wiki/Free_will_theorem