Classical probabilistic rounding error analysis is particularly well suited to stochastic rounding (SR), and it yields strong results when dealing with floating-point algorithms that rely heavily on summation. For many numerical linear algebra algorithms, one can prove probabilistic error bounds that grow as $\mathcal{O}(\sqrt{n}u)$, where $n$ is the problem size and $u$ is the unit roundoff. These probabilistic bounds are asymptotically tighter than the worst-case ones, which grow as $ \mathcal{O}(nu)$. For certain classes of algorithms, SR has been shown to be unbiased. However, all these results were derived under the assumption that SR is implemented exactly, which typically requires a number of random bits that is too large to be suitable for practical implementations. We investigate the effect of the number of random bits on the probabilistic rounding error analysis of SR. To this end, we introduce a new rounding mode, limited-precision SR. By taking into account the number $r$ of random bits used, this new rounding mode matches hardware implementations accurately, unlike the ideal SR operator generally used in the literature. We show that this new rounding mode is biased and that the bias is a function of $r$. As $r$ approaches infinity, however, the bias disappears, and limited-precision SR converges to the ideal, unbiased SR operator. We develop a novel model for probabilistic error analysis of algorithms employing SR. Several numerical examples corroborate our theoretical findings.

Computer-assisted proofs (CAPs) have become an essential tool for rigorously validating mathematical results, particularly in fields where pen-and-paper analytical approaches alone prove challenging. In this talk, we will first discuss a posteriori validation methods; that is, CAP techniques designed to certify numerical solutions and establish rigorous bounds on computational errors. Then, we will explore the broader impact of CAPs, particularly in the study of delay maps derived from delay differential equations (DDEs) of the form $ y’(t) = \alpha y(t) + g(y(t − \tau))$. DDEs are naturally set on infinite-dimensional spaces and as such, even scalar equations exhibit rich dynamics. The approach integrates Chebyshev series expansions to rigorously evaluate the delay map. The discussion will include a case study on the Mackey-Glass equation, and its long-standing conjecture related to chaotic dynamics. Finally, we will outline some future directions for rigorous numerics, the next steps in software development, and ongoing challenges in advancing the field.