11·
16 hours agoThe number of self-driving cars and trucks has been roughly doubling year over year, there are around 5000 right now.
FWIW, I don’t think we will ever see safe in all driving conditions, there are plenty of driving conditions where it is fundamentally unsafe for cars and no man nor machine should be driving in them, so in your particular case, you get to wait for self driving cars for the rest of your life.
I think in 5 years people will be complaining about a lack of available open-source and self-hosted self-driving cars, but safe in all weather? Probably not.
You know what all those methods have in common? FUCKING evaluation of smooth continuous functions based on a limited number of samples.
REAL MEN WRITE REAL PROOFS. They don’t use God damned computational methods which completely IGNORE non-converging regions.
I used opus to generate this lean-verifiable proof that you in particular are full of shit!
import Mathlib open Real noncomputable def f (x : ℝ) : ℝ := sin (π * x) * exp (-x^2) lemma f_smooth : ContDiff ℝ ⊤ f := (contDiff_sin.comp (contDiff_const.mul contDiff_id)).mul (contDiff_exp.comp (contDiff_id.pow 2).neg) lemma f_zero_on_ints : ∀ n : ℤ, f n = 0 := by intro n show sin (π * (n : ℝ)) * exp (-((n : ℝ))^2) = 0 rw [mul_comm π (n : ℝ), sin_int_mul_pi, zero_mul] lemma f_ne_zero : f ≠ 0 := fun h => by have h₁ : f (1/2) = 0 := congrFun h (1/2) have h₂ : f (1/2) = exp (-(1/2)^2) := by show sin (π * (1/2)) * exp (-(1/2)^2) = exp (-(1/2)^2) rw [show π * (1/2) = π/2 from by ring, sin_pi_div_two, one_mul] exact (exp_pos _).ne' (h₂ ▸ h₁) theorem sampling_is_a_lie : ∃ f : ℝ → ℝ, ContDiff ℝ ⊤ f ∧ (∀ n : ℤ, f n = 0) ∧ f ≠ 0 := ⟨f, f_smooth, f_zero_on_ints, f_ne_zero⟩