mcshicks
Joined 11 years ago
Karma
501
Submissions
266
Member since
Jan 8
Recent submissions
Comment · 26 days ago
Comment · 1 month ago
I'm getting on a plane tomorrow. I think I would prefer a world with the FAA than one without it.
Comment · 1 month ago
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.
Comment · 2 months ago
This set of videos from eevblog worked for me.
Comment · 2 months ago
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...
Comment · 2 months ago
Umm I would say working physical samples is pretty important.
Comment · 3 months ago
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.
Comment · 6 months ago
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...
Comment · 1 year ago
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"
Comment · 1 year ago
Surprised there was no mention of brief. That was my favorite editor for programming for a while.
Comment · 1 year ago
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.
Comment · 1 year ago
I think the name refers to the limits some airlines have. JAL for instance offers one hour free on some flights.
Comment · 1 year ago
In the US there is a bill that's been floating around Congress for a while called the improving digital identity act.
https://www.congress.gov/bill/118th-congress/senate-bill/884...
Comment · 1 year ago
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
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.