skysight-inc/HackerNews huggingface dataset:
The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I challenge you to do it in fewer than 30 moves. I should also say that whilst Metamath has certainly formalised a whole bunch of mathematics, it has not remotely gone "a long way" by any reasonable measure which a mathematician would use. For example, how much of an undergraduate mathematics curriculum does it have? How much representation theory? None. How much differential geometry? None. How much commutative algebra? Epsilon. These are the measures which mathematicians use, not lines of code. It is time that formalisation started to appeal to mathematicians, and for this to happen it is essential that it starts to demonstrate that it can actually do a lot of the kind of mathematics which is recognised as "completely standard undergraduate material and hence trivial" by mathematicians. It is still the case that these systems cannot do certain things which were known to Gauss or Euler (for example it was only this year that Lean learnt the proof that the class group of an imaginary quadratic field was finite, and as far as I know no other system at all has class groups -- but we teach this to the undergraduates!). Just saying "large code base therefore we've gone a long way" is not the correct logic. The question is how much of it is recognisable as worth teaching to undergraduates in 2021, and conversely how much stuff worth teaching to undergraduates in 2021 is _not_ in any of these systems. That's where the problems begin to show up. In Lean we are well into a project of formalising an entire undergraduate curriculum and within about two years we will have finished.
Show HN: Try Snowplow
More like selectively scrubbing news and politics, this case in point being one more example to add to this troubling trend.
Snowplow has had a strong following around HNers ever since we launched back in 2012. The truth is though that Snowplow open-source is still a complex project to stand up, and a lot of technology teams still aren't aware of the power of having all their own behavioral data (events from webapps, mobile etc) in their own data warehouse or lake, and available in real-time streams (Kinesis and GC Pub/Sub).

With this background, I am delighted to be able to Show HN our new Try Snowplow experience. Under lockdown last year, the team decided to go back to basics and build a new version of Snowplow called Try Snowplow; that version is now in GA.

Try Snowplow is a small version of the Snowplow technology that can be setup quickly and easily - normally under 15 mins. Like all versions of Snowplow, it runs in your own cloud environment.

The landing page is here: https://snowplowanalytics.com/get-started-try-snowplow/

And if you want to learn more about Try Snowplow before giving it a spin, there's a video here: https://www.youtube.com/watch?v=Aw5hdIjwVhY&ab_channel=Snowp...

If you are still puzzled why you want your own behavioral data in your own warehouse, check out our library of use cases here: https://snowplowanalytics.com/use-cases/

Any questions just shout! Happy to answer anything Snowplow-related, and thanks again for Hacker News' support of Snowplow over the years.
This is a solid reply, thanks.

I like those middle 2 lines; for a user of a free OS, Mac hardware is interesting, but the reverse is not true.

And sure, "use whatever OS you want" is kind of my point too. I have seen the Mac community at large seeming to not have that live and let live attitude. Not anyone on this thread, but I think it is a thing that happens.
>meanwhile wealth was unnecessarily transferred weighted towards the earliest adopters.

How many companies and technologies is this true or? Does this make them all MLM schemes?

Nothing about your response indicates you're giving me a generous interpretation at all, especially given how much of this response is you dumping rhetoric on me. Being snarky and in the same breath elaborately calling me "holier-than-thou" seems like we're just going to have a name calling arms race.

Similarly, the notion that more intelligent people are 'sucked in and defensive' is the true explanation, and you don't seem receptive to another interpretation to intelligent people thinking a technology is promising...it seems we may as well just leave it here. Thanks for your time.
Because she was gaining more support/momentum, and she is going toward the direction the military doesn't like.

The coup proves that she never really had any authority to begin with.
How is keeping compatibility with a historic set of libraries simple?
The difference is social-analyzer is free and open source.
Commenting vs. Making
> "what do we expect some of the new problems to be?"

A name for this I’ve heard (and use) is the “pre-mortem”; you can get folks in the right headspace for what you are suggesting by asking them to imagine they are writing a post-mortem after the proposed initiative failed.

A good way of surfacing failure modes / potential quagmires.
Recommended "literature":

1. 10 Things I Regret About Node.js - Ryan Dahl - JSConf EU (https://www.youtube.com/watch?v=M3BM9TB-8yA)

2. Brendan Eich: JavaScript, Firefox, Mozilla, and Brave | Lex Fridman Podcast #160 (https://youtu.be/krB0enBeSiE)
Yes! I work at a FAANG and over my time here it's been C++, Java, Python, and JS. The least "boring tech" part of my work has probably been that were moving from JS to Typescript? Mostly, we want to use things that we're confident can do what we need, and that we're confident don't have hidden surprises.
I would be interested to know why the RFC 1035 forbids using IP addresses in MX records. What was the original concern with doing this?
The salary is just so much easier to quantify

The constant learning just to stay up to date? Isn’t that part of the other professions too?
My take on Doug's vision - having worked with him for a few years before his untimely departure:
While he is celebrated for the mouse, windows, and other ideas coming out of his lab, he should be better understood, not for the MotherOfAllDemos, but for what it meant (my opinions):
He spoke of the ABC architecture, where "C" work is the production line, "B" work is facilitating and improving C work, and "A" work is improving B work.

"A" work is where the concept flourishes: he spoke of networked imrovement communities (NICs) where the "A" team is an improvement community, and a NIC is those "A" teams in a network. Think IEEE as a NIC.

But, he didn't stop there. What is an improvement community? My interpretation is that he uses the term "Dynamic Knowledge Repository" (DKR) to explain the A team; "repository" does not refer to a bank account; rather, a DKR is a combination of human systems, tool systems, and the knowledge brought to the table by the humans. Draw a circle around that. That's how I interpret a DKR.

Key point to take home: all of the elements of a DKR are in a state of continuous coevolution. As humans improve, the tools they use must rise to the occasion.

What held back that concept, historically, has been the tool systems. When he did MOAD, I was working at IBM on OS 360 mainframes. That's what we had in the 60's. Today, my cell phone has more compute power and memory than one of the 360s I serviced back then.

It's for that reason that I am optimistic that we are on a path to realizing Doug's grand vision; our tool systems are now way ahead of we humans.
A 1x1x1 km landfill (they are actually holes in the ground) can contain the entire waste of the US for three years. How many of those can we hide in the western US without anyone ever noticing? Howa bout a 100x100 km patch, that will hold 30,000 years worth of trash. Meanwhile we can focus our energy on the only problem that really matter - the climate problem.
They normally have high-speed cameras running; that short video is a mish-mash of super-slow-mo and regular speed footage. There are much longer versions on YT, e.g. this one [0] which covers it in more detail (watch the people in the room jump when it blows - despite being a fair distance away).

[0] https://www.youtube.com/watch?v=j973645y5AA
in a time when institutions and experts are failing all around us, I appreciate your optimism. but it's too much like a blind faith and devotion to priests for my tastes.

and maybe they are right about every regulation, that's a possibility! but clearly something has gone wrong when we could have had a clean grid powered via nuclear energy by now. so I think it would be wise to question everything in the chain.
Is there a need for browser-level support for math formulas anymore? https://www.mathjax.org/ is a good support library if you want math in your webpage and don't want to resort to images. I've used it with https://casual-effects.com/markdeep/features.md.html#embedde... and haven't had any issues.
Firefox's PIP has to be the browser's single most useful feature in recent years for me.
The Four Colour Theorem in Coq seems pretty mainstream I'd say... Also I guess you know that you don't personally have to reject LEM to use Agda or whatever, you just can't do everything in it or at least everything the classical way.
The UK government introduced a test to check how children were progressing in phonics. Teachers were told the pass mark to aid in assessment, but the national results showed a remarkable bump for exactly the pass mark:

https://schoolsweek.co.uk/phonics-check-needs-rethink-after-...

The government decided to not share the pass mark ahead of time for tests in future years. I attended a conference that year at which the Education Secretary gave a keynote to an audience of educators; he got booed for not trusting teachers as a result.
References please.
I don't think that happens anymore?
You've already been told about ALSA (which Pulse uses and organizes, for its the low-level audio subsystem the kernel offers) and Jack, which specializes in low-latency audio. There's also sndio ported from OpenBSD.

But the one you might want to consider instead is called PipeWire. It implements the ALSA, Pulse and Jack APIs with a single implementation and it's pretty much the future of audio (and video casting) on Linux.

If you're using Wayland, you're already using PipeWire, but likely not for audio. On Fedora you can follow the instructions here https://fedoraproject.org/wiki/Changes/DefaultPipeWire which basically boil down as "uninstall pulse and install these packages" and you'll be using PipeWire for your audio.

I had tried several times to switch to it and it was not ready, but about a week ago I've been able to make the move with no loss in functionality and even got a fix to an old bug that affected my sound card, so at least with version 0.3.22 I can recommend giving it a go. Switching back to Pulse if bugs arise is trivial anyway.
Userids are only one of thousands of signals that can identify accounts
It seems like author took too much of the responsibility, like 10X dev. Its better to take less responsibility with slightly above average salary and get more of personal time.. this reminds of a story about fish finding for ocean from a movie Soul
Yeah the distance thing was ball parked, based on the last time I ran the numbers. To your point, I accidentally omitted to say “round trip from SF to NY” - I also used the great circle distance (2586mi) and ballparked a phone at 200g, roughly the weight of an iPhone.

Thank you for going through the numbers and adding the sources. I was on my phone and meant to circle back.
A Professional Video Tool “ a Must Have ”
Not sure about the UK, but in the US, it's the opposite. Failing schools get more funding, at least temporarily, with the expectation they turn the scores around in a few years. They risk losing accreditation if they don't improve, but that's usually years away.
Cheapest but toughest way is SBA [0] Financing through traditional banks. You get the lowest interest rates (usually Prime + 1-2% extra) with upto 10 years of payment term. The problem is that it can take 2-3 months with tons of documentation and a personal guarantee if you are small. I have some experience with this for our own SAAS so happy to share more if needed.

I wouldn't rule SBA backed loans out because the more expensive options may give you capital faster but you pay a lot more premium. And when I say "lot more", I mean "a hell of a lot more premium"..

[0] https://www.sba.gov/funding-programs/loans
> Inner city districts are usually near the top of their state for per pupil spending

does this include donations and other sources of revenue (eg. bake sales)?
> I find them out of place (mixing cute things with technical matters)

I love beautifully engineered software that's represented by a whimsical cartoon character or other non-vector-perfect hand-drawn art.
Why not follow the standards? The standard states a MX record contains a domain name that does not point to a CNAME record.

If you don’t follow the standards things might fail. That’s not someone else’s fault, it’s your fault.
Same with CD. I had a SONY car changer.

It would play literally anything. Seriously, I found a Bare Naked Ladies CD on the ground. Scuffed to a point of doom.

For grins, I put it in the SONY, and it took a bit longer to buffer up, but just worked!

That same disc would not play in any other device I had.

I get the feeling the more robust error correction was not implemented on most devices.
Samsung TVs are so horrible with spyware that it is best to keep them off the network and use an attached device like a Shield or Roku. This is also true with most other "smart TVs"
I agree that Google is still just a better search engine, and that sucks. But I still try to do my search on DDG first -- if I find what I'm looking for, great! If I haven't found it after a few seconds, I open Google and search there. At most, I've wasted a few seconds. But even if it means Google has some data on me, if I can divert 40% (or more) of my searches to DDG, that's 40% less data Google has on my search history.
That's good to know. Do you have a source handy?
> resolutely non-classical approach

Calling this 'non-classical' is interesting—it's definitely non-classical from the point of view of formalisation, but I'm not sure formalisation has been around long enough to have classics ….

As of course you know but non-mathematicians may not, from a non-formalising mathematician's point of view, it's the non-constructive logic that's classical, to the extent that it's actually sometimes called classical logic (https://en.wikipedia.org/wiki/Classical_logic).
You're taking his words out of proportion. Just by looking at the steam hardware survey you'll see that the majority of gamers buy mid range cards and own 1080p monitors. The most popular games aren't the latest AAA titles either.

There isn't a game option survey but I'd bet most gamers with mid range cards run AAA games on medium as they value being able to play over a beautiful slideshow.
> The salary is just so much easier to quantify

He only briefly mentioned that though and it was not the main point.

> The constant learning just to stay up to date? Isn’t that part of the other professions too?

Depends on the profession of course, but generally speaking, no. No other profession changes every five minutes (exaggerated of course), even IT did not up until 10, 15 years ago.

As I mentioned already, the OP might have simplified things, but overall I agree with him.
Because you'd immediately get called out/canceled for being racist.
Thanks for explaining this. I appreciate the effort you've put into this, and this is certainly something I've always wanted browsers to support. One suggestion: is it possible to see the tabs next to each other in the same window? Something like "splitting" the window in VS Code.
Then the root private key gets extracted, because there's lots of money to be had from doing so
NANO has delegated Proof-of-Stake. It's the representatives who vote on transactions. And it's supposed they don't have incentives to ruin the network. It's true, but a single representative can be captured by villains, who CAN have incentives to ruin the network.

I actually like NANO, their blockchain structure is certainly next level, but it also has vulnerabilities due to PoS consensus.
Yes, that's what I understand too. I believe since I have a direct blood relation that neither me nor my kids would need to do those tests but my wife would. But I wasn't sure if I would need to visit the consulate. Definitely tricky to pull off these days.

Looks like you lived in Padova for quite some time. I was there for 6 months or so back in 2003. Would love to visit again. My family there is mostly in Milano but from Cuneo and Sardegna. :)
Thanks for sharing. I love it. Might add it to the food plan !;)
Doesn't this get boring at some point? By now everyone should be aware of the implications of using Facebook/Instagram/WhatsApp and they still use it. Must it be the pure evilness of Facebook which manipulates the whole world or might it be possible that they are actually providing value to people?
Okay, lets say we agree that the sports industry causes externalities. The sports industry recognizes this and installs LEDs and other efficient electronics and cuts their energy consumption by 50%. If the sports industry and Bitcoin were equivalently bad the sports industry would immediately respond to the efficiency increase by doubling the number of stadiums and consume the same amount of energy in the end. Worse, they also had to construct new stadiums with concrete and therefore emitted CO2 during the construction process.
I use gammu-smsd and forward it to iOS using Pushover.

For the serial AT modem I use random Huawei LTE USB stick that I bought for 15 EUR years ago.

It was so cheap because it was provider locked, but there are keygens floating around internet that allow unlocking it to work on any network.
Blu-ray elevates it quite poorly. I recently bought a Terminator set where it forced a 3 minute spiel on the blu-ray format on several discs (I couldn't know about it's AMAZING quality after having bought a whole set of them /s).

I just buy to rip/collect, but sometimes I have to navigate menus on a physical player to match features and titles. Lots of releases out there force previews, anti-piracy warnings, ridiculous menu sequences, and a whole host of other content that detracts from the experience.

https://en.wikipedia.org/wiki/User_operation_prohibition
Is Clojure a boring technology yet? :)
Ask HN: Help me write a technical test that doesn't suck
Every technical test that I've had during my career has totally sucked. I've attempted to improve on that here:

https://github.com/philbert/take-home-tech-test

I've been the interviewer far more times that I've been the candidate, but during my reflections, what I've learned about technical tests and technical interviews are the following:

1. Most interviewers try to hire themselves. That is to say, they are heavily biased toward asking questions they already know the answer to, rather than trying to find the candidate's strengths.
2. If I don't think your take-home technical test is fun, I'm not going to do it.
3. Even though 99% of the code I've written isn't public and probably never will be, I have enough code on Github that I should be able to just submit my account as my "technical submission" into your recruitment process.

The test isn't perfect but I'm now in the second set of interviews where we've used it and it has worked quite well.

I would love to hear some feedback to help me improve it.
I notice this is using the AGPL but it isn't a web application. How is using the AGPL in this situation different from just using the GPL in terms of how it affects software that uses it? Does any public facing web application that uses this library need to be released under the AGPL?
> and choosing to use ETH2 as their mainnet substrate chain instead.

But why exactly? Until ETH1 is in the ETH2 chain ecosystem ETH2 is just another blockchain platform, providing no network effects.

ETH2's big selling point was higher throughput but bridges are already starting to commoditize access to more throughput from ETH1. ETH2 could provide smoother access than the bridge interfaces provided by other chains. (I'm speaking of bridges both to and from ETH1 and within the bridge blockchain's ecosystem like IBC)

It's not that I don't think ETH2 could win this. There's a clear path to victory.

- ETH1 integrated ASAP, going all in on expanding ETH1 capacity and bringing it under ETH2

- Provide a subchain interface that's better than IBC or any other cross-chain interface on the market

- Fullnode tooling that really works well (partial syncing for block availability, seamlessly syncs multiple chains etc)

Once you have these you can keep ETH1 users via network effect and provide access to more capacity more easily than other potential platforms.

But I don't see a clear plan from ETH2 to do either of those things. Cross chain communication is a theory-only problem devoid of the extremely polished tooling it will need to win and ETH1 under the beacon chain doesn't even seem to have a plan.
OLED looks promising.

For me the big things are speed and the color gamut glowing phosphors in tubes can deliver. Plasma and CRT displays have great color and are fast.

Scan lines are cool too.

Other things, blooming on super bright, or high contrast are less desirable, but yeah. I would enjoy seeing things in that way myself.
this is very cool.

another interesting open-source project for imperfect-information game solving is DeepMind's OpenSpiel:

https://github.com/deepmind/open_spiel

However as far as poker goes, I believe they only provide toy versions of the game, even though theoretically you could put in your own implementation.

I've noticed that in this part of the AI world, things tend to be closed-source for whatever reason and I think that limits the ability to learn. Seems good to see that changing.
> happily keep you in that same situation for years

happily keep you === happily stay
> Like literally every other piece of Bitcoin or crypto mining technology.

I don't get this comparison because Nvidia isn't a Bitcoin mining technology company. Or at least they weren't until a week ago. When someone deems it not profitable to mine on a set of 50 GPUs they purchased, they can resell those to gamers. But these mining cards are just e-waste.

> Don’t hate the player; hate the game.

Games don't exist without players.
> You’re making a huge assumption that they could be resold, even if they’re the same chips. This could be an entirely new market for chips that have yield defects in the graphics units, that will not ever work for games, and were previously already put in the trash.

Chip binning is nothing new, the article even explains this phenomenon.
I totally agree with you on this and this is why most companies loose on innovation.

And they loose competition with other players in the market. For example companies like Nokia, Blackberry and etc
A Word to the Resourceful (2012)
No, it's probably just a good idea to remind people of this feat, similarly to the legendary wrestling match in nineteen ninety-eight when The Undertaker threw Mankind off Hell In A Cell and plummeted 16 ft through an announcer's table.
Right, so what’s their volume on a100s and are they a favored mining tool? If so, I think that might be the disconnect between what people think nvidia is focused on, and what they are focused on.

Plus, I’ll point out that a lot of information can be hidden by public companies. Amazon was pretty quiet about it’s growth in sales of AWS as a dominant force for a number of years.