mcshicks
mcshicks on Hacker News
"not at the Lean code, since I know very little of the actual usage of Lean, and that code was enormous"
This part I don't understand. Not that anyone should read the entire Lean code of any proof, but if the statement of the theorem to be proven in lean seems to be correct, then I would think there would be at least some interest if in fact there was a formal proof (which might or might not correspond to the written proof) of something I was working on. That to me would be interesting. Or you are saying you doubt the validity of the formal proof, which would also be interesting. But saying it is of no consequence doesn't make any sense to me.
I'm getting on a plane tomorrow. I think I would prefer a world with the FAA than one without it.
I think there is an obvious example in the FAA of a successful safety regulation of another potentially dangerous technology industry. A similar agency would seem to me like a logical starting point. I did some minor work a long time ago in commercial avionics software and while it was a very tedious process I did have confidence in it. Obviously a lot of things would have to be different but the basic structure of development and testing standards, record keeping, transparency, and government incident investigation seems like the place to start.
Did you read it?
89. Living out justice in the Church means purifying ecclesial relationships and structures from distortions that give rise to inequality, lack of transparency and abuse of power. In this regard, listening to the victims of spiritual, economic, institutional, sexual and power-based abuse, as well as abuses of conscience, is an integral part of a journey toward justice, which includes acknowledging the harm done, just reparation and taking steps to prevent it from happening again. Every power is at the service of communion and mission. All authority is at the service of the People of God. This ministry of service is expressed not only through our faith celebrated and lived in the Sacraments, and in the adoption of a synodal style, but also in the concrete sharing of goods. Following the example of the early Church, ecclesial resources need to be shared so that no one among us may be in need (cf. Acts 434, and so that their administration may support the mission of proclaiming the Gospel to the poorest. Regular assessments of the exercise of ministerial responsibilities should be encouraged, not as judgments on individuals, but as tools for learning and correction oriented toward mission. 116 Only to the extent that we are open to the action of the Holy Spirit will these principles of Social Doctrine become incarnate in ecclesial life. In this way, the Church will be able to bear credible witness to society that seeking the common good together, with shared responsibility and fraternity, is not a utopia, but a real possibility.
https://www.vatican.va/content/leo-xiv/en/events/event.dir.h...
Umm I would say working physical samples is pretty important.
It is Kevin Buzzard. It's kinda small font on my phone but if you look at the "about xena" link it says it's his site.
There have been bills in the past like "The improved digital identity act of 2023" that never get out of committee. The latest incarnation seems to be "H.R.7270 - Stop Identity Fraud and Identity Theft Act of 2026". There almost always have one republican and one democratic sponsor. But they don't seem to rise to the level of urgency to get past the current dysfunction in congress.
https://www.congress.gov/bill/119th-congress/house-bill/7270...
They seemed to have missed peter turchin
"In 2010, Turchin published research using 40 combined social indicators to predict that there would be worldwide social unrest in the 2020s"
https://en.wikipedia.org/wiki/Peter_Turchin
Pretty sure it will work on JAL at least right now. They just asked for an email. But it was also a new service so maybe to wanted people to try it. It occurred to me at the time that two devices with two emails should work for twice as long. For what I wanted to do on that flight, i.e. check and send a few messages the one free hour was fine. But yeah of course they could change it so that would not work.
I think the name refers to the limits some airlines have. JAL for instance offers one hour free on some flights.
You can run the model for free on openrouter.ai. I have played around with lean, slowly working my way through mathmatics in lean. I was stuck on this problem in section 3.6
theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ}
(sa : ConvergesTo s a) (sb : ConvergesTo s b) :
For fun I tried it on the free model on openrouter.ai. Got the answer the first time.
https://leanprover-community.github.io/mathematics_in_lean/m...
Here's the answer just to give you a feel.
by_contra h
have h₁ : a ≠ b := h
have h₂ : |a - b| > 0 := by
apply abs_pos.mpr
exact sub_ne_zero.mpr h₁
-- Use the definition of convergence to find N₁ and N₂
have h₃ := sa (|a - b| / 2) (by linarith)
have h₄ := sb (|a - b| / 2) (by linarith)
cases' h₃ with N₁ h₃
cases' h₄ with N₂ h₄
-- Choose N to be the maximum of N₁ and N₂
let N := max N₁ N₂
have h₅ := h₃ N (by simp [N, le_max_left])
have h₆ := h₄ N (by simp [N, le_max_right])
-- Derive a contradiction using the triangle inequality
have h₇ : |s N - a| < |a - b| / 2 := by simpa using h₅
have h₈ : |s N - b| < |a - b| / 2 := by simpa using h₆
have h₉ : |a - b| < |a - b| := by
calc
|a - b| = |a - s N + (s N - b)| := by ring_nf
_ ≤ |a - s N| + |s N - b| := by
apply abs_add
_ = |s N - a| + |s N - b| := by
rw [abs_sub_comm]
_ < |a - b| / 2 + |a - b| / 2 := by
linarith
_ = |a - b| := by ring
linarith
That's so funny I had to check something was working with an llm API last night and that's what I asked it, but just in jest.
I find the most consistent explanation for Donald Trump is he does whatever is going to keep himself the top news story in the media. I don't think there's any deeply held belief other than if he doesn't think people are talking about him that's bad
I was going to say I have a old twiddler 2 (wired usb). There was this program I used to learn called "twidor" that was like a type tutor but had graphic that showed you the chords. Really helpful. I didn't see anything like that in the github repository linked in the video. I guess they are up to twiddler 4 now. I read the linked chordite page and I agree that a problem with the twiddler is you are kind of trying to hold the thing steady so you can chord with the same fingers you chording with.
https://wearables.cc.gatech.edu/projects/twidor/screens.html
I don't know, it's hard for me to know what the author means by "fundamentals". I looked at the table of contents from the amazon website, and somethings that I consider pretty fundamental like Thevenin's Theorem didn't seem to be listed there. By comparison it's in Chapter 1, page 9 on my copy of "The Art of Electronics". I'm not trying to knock the book, it could be very handy, but I would use the term "basics" as opposed to "fundamentals" to describe the content as I understand it.
I have a twiddler and tried doing this a long time ago i.e. emacs with a twiddler. For me I really needed to use a sticky cntl and alt key because I just couldn't press the cntl button on the top and chord at the same time. And I couldn't figure out how to make the sticky cntl work on the phone. But that was a very long time ago. Now I just use a mini bt keyboard and termux to run emacsclient over ssh and that's good enough for what I want.
Tailscale, ssh and emacsclient in terminal mode makes it pretty easy to access and update notes from different machines without syncing by just say leaving your main laptop on and connected to the Internet and using emacs daemon. If you have sshd running on all the machines you can use tramp to move files around or use git or many other tools. The trickier part is using emacs key bindings on say android. Read only sharing with PDFs works fine. Co editing is impossible :).
Honest question. What's happens to Microsoft's investment then?
Exactly what I want know! A non profit is a corporation for public benefit. They bylaws state how the board gets elected, but there is no such thing as voting shares. So there is no owner. When you close a non profit you have to disperse the assets to another entity that supports the non profits mission statement.
I guess it matters how long it is and if you need to know it exactly, and how long you need to retain it. I had to memorize 50 to 100 word phrases and I chained them together with index cards. The first sentence is the cue for the second, the second for the third, etc. Carried them around in my pocket in order and started from first a few times a day until I could do the whole thing. But I only needed to know it exactly for a few weeks usually.
Maybe if you are a non profit based in CA. There's probably some other corner cases I'm not aware of, like it might be simpler in some cases like an LLC for holding family property, etc.
It means the child of a first cousin. I'm a native speaker of English and I find the phrase confusing also.
Hey I'm a long term emacs/org mode user. This look super interesting, one quick suggestion, even though I'm confident I can make the installation instructions work, a lot of people just install packages from melpa, i.e. list-packages, cntl-s to find in melpa and then install. I know there's a lot of advantages to some other methods, but people pick and choose where they want to learn the new way or stick with old tried and true way. Again at first glance it looks super interesting.