Shuonan Wu

Qingguo Hong, Fei Wang, Shuonan Wu et al.

A unified study is presented in this paper for the design and analysis of different finite element methods (FEMs), including conforming and nonconforming FEMs, mixed FEMs, hybrid FEMs,discontinuous Galerkin (DG) methods, hybrid discontinuous Galerkin (HDG) methods and weak Galerkin (WG) methods. Both HDG and WG are shown to admit inf-sup conditions that hold uniformly with respect to both mesh and penalization parameters. In addition, by taking the limit of the stabilization parameters, a WG method is shown to converge to a mixed method whereas an HDG method is shown to converge to a primal method. Furthermore, a special class of DG methods, known as the mixed DG methods, is presented to fill a gap revealed in the unified framework.

Jinchao Xu, Yukun Li, Shuonan Wu et al.

We study in this paper the accuracy and stability of partially and fully implicit schemes for phase field modeling. Through theoretical and numerical analysis of Allen-Cahn and Cahn-Hillard models, we investigate the potential problems of using partially implicit schemes, demonstrate the importance of using fully implicit schemes and discuss the limitation of energy stability that are often used to evaluate the quality of a numerical scheme for phase-field modeling. In particular, we make the following observations: 1. a convex splitting scheme (CSS in short) can be equivalent to some fully implicit scheme (FIS in short) with a much different time scaling and thus it may lack numerical accuracy; 2. most implicit schemes (in discussions) are energy-stable if the time-step size is sufficiently small; 3. a traditionally known conditionally energy-stable scheme still possess an unconditionally energy-stable physical solution; 4. an unconditionally energy-stable scheme is not necessarily better than a conditionally energy-stable scheme when the time step size is not small enough; 5. a first-order FIS for the Allen-Cahn model can be devised so that the maximum principle will be valid on the discrete level and hence the discrete phase variable satisfies $|u_h(x)|\le 1$ for all $x$ and, furthermore, the linearized discretized system can be effectively preconditioned by discrete Poisson operators.

Fei Wang, Shuonan Wu, Jinchao Xu

In this paper, we study a mixed discontinuous Galerkin (MDG) method to solve linear elasticity problem with arbitrary order discontinuous finite element spaces in $d$-dimension ($d=2,3$). This method uses polynomials of degree $k+1$ for the stress and of degree $k$ for the displacement ($k\geq 0$). The mixed DG scheme is proved to be well-posed under proper norms. Specifically, we prove that, for any $k \geq 0$, the $H({\rm div})$-like error estimate for the stress and $L^2$ error estimate for the displacement are optimal. We further establish the optimal $L^2$ error estimate for the stress provided that the $\mathcal{P}_{k+2}-\mathcal{P}_{k+1}^{-1}$ Stokes pair is stable and $k \geq d$. We also provide numerical results of MDG showing that the orders of convergence are actually sharp.

Shuonan Wu, Jinchao Xu

In this paper, we propose a family of nonconforming finite elements for $2m$-th order partial differential equations in $\mathbb{R}^n$ on simplicial grids when $m=n+1$. This family of nonconforming elements naturally extends the elements proposed by Wang and Xu [Math. Comp. 82(2013), pp. 25-43] , where $m \leq n$ is required. We prove the unisolvent property by induction on the dimensions using the similarity properties of both shape function spaces and degrees of freedom. The proposed elements have approximability, pass the generalized patch test and hence converge. We also establish quasi-optimal error estimates in the broken $H^3$ norm for the 2D nonconforming element. In addition, we propose an $H^3$ nonconforming finite element that is robust for the sixth order singularly perturbed problems in 2D. These theoretical results are further validated by the numerical tests for the 2D tri-harmonic problem.

Shihua Gong, Shuonan Wu, Jinchao Xu

In this paper, we present a family of new mixed finite element methods for linear elasticity for both spatial dimensions $n=2,3$, which yields a conforming and strongly symmetric approximation for stress. Applying $\mathcal{P}_{k+1}-\mathcal{P}_k$ as the local approximation for the stress and displacement, the mixed methods achieve the optimal order of convergence for both the stress and displacement when $k \ge n$. For the lower order case $(n-2\le k<n)$, the stability and convergence still hold on some special grids. The proposed mixed methods are efficiently implemented by hybridization, which imposes the inter-element normal continuity of the stress by a Lagrange multiplier. Then, we develop and analyze multilevel solvers for the Schur complement of the hybridized system in the two dimensional case. Provided that no nearly singular vertex on the grids, the proposed solvers are proved to be uniformly convergent with respect to both the grid size and Poisson's ratio. Numerical experiments are provided to validate our theoretical results.

Shuonan Wu, Yukun Li

The paper analyzes the Morley element method for the Cahn-Hilliard equation. The objective is to derive the optimal error estimates and to prove the zero-level sets of the Cahn-Hilliard equation approximate the Hele-Shaw flow. If the piecewise $L^{\infty}(H^2)$ error bound is derived by choosing test function directly, we cannot obtain the optimal error order, and we cannot establish the error bound which depends on $\frac{1}ε$ polynomially either. To overcome this difficulty, this paper proves them by the following steps, and the result in each next step cannot be established without using the result in its previous one. First, it proves some a priori estimates of the exact solution $u$, and these regularity results are minimal to get the main results; Second, it establishes ${L^{\infty}(L^2)}$ and piecewise ${L^2(H^2)}$ error bounds which depend on $\frac{1}ε$ polynomially based on the piecewise ${L^{\infty}(H^{-1})}$ and ${L^2(H^1)}$ error bounds; Third, it establishes piecewise ${L^{\infty}(H^2)}$ optimal error bound which depends on $\frac{1}ε$ polynomially based on the piecewise ${L^{\infty}(L^2)}$ and ${L^2(H^2)}$ error bounds; Finally, it proves the ${L^\infty(L^\infty)}$ error bound and the approximation to the Hele-Shaw flow based on the piecewise ${L^{\infty}(H^2)}$ error bound. The nonstandard techniques are used in these steps such as the generalized coercivity result, integration by part in space, summation by part in time, and special properties of the Morley elements. If one of these techniques is lacked, either we can only obtain the sub-optimal piecewise ${L^{\infty}(H^2)}$ error order, or we can merely obtain the error bounds which are exponentially dependent on $\frac{1}ε$. Numerical results are presented to validate the optimal $L^\infty(H^2)$ error order and the asymptotic behavior of the solutions of the Cahn-Hilliard equation.

Yuchen Jiang, Ruo Li, Shuonan Wu

A multi-scale method for the hyperbolic systems governing sediment transport in subcritical case is developed. The scale separation of this problem is due to the fact that the sediment transport is much slower than flow velocity. We first derive a zeroth order homogenized model, and then propose a first order correction. It is revealed that the first order correction for hyperbolic systems has to be applied on the characteristic speed of slow variables in one dimensional case. In two dimensional case, besides the characteristic speed, the source term is also corrected. We develop a second order numerical scheme following the framework of heterogeneous multi-scale method. The numerical results in both one and two dimensional cases demonstrate the effectiveness and efficiency of our method.

Shaonan Wu, Shuai Lu, Yeyun Gong et al.

Formal proofs are challenging to write even for experienced experts. Recent progress in Neural Theorem Proving (NTP) shows promise in expediting this process. However, the formal corpora available on the Internet are limited compared to the general text, posing a significant data scarcity challenge for NTP. To address this issue, this work proposes Alchemy, a general framework for data synthesis that constructs formal theorems through symbolic mutation. Specifically, for each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. Subsequently, we mutate the candidate theorem by replacing the corresponding term in the statement with its equivalent form or antecedent. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M. Furthermore, we perform continual pretraining and supervised finetuning on this augmented corpus for large language models. Experimental results demonstrate the effectiveness of our approach, achieving a 4.70% absolute performance improvement on Leandojo benchmark. Additionally, our approach achieves a 2.47% absolute performance gain on the out-of-distribution miniF2F benchmark based on the synthetic data.To provide further insights, we conduct a comprehensive analysis of synthetic data composition and the training paradigm, offering valuable guidance for developing a strong theorem prover.

Shuonan Wu, Shihua Gong, Jinchao Xu

We propose two classes of mixed finite elements for linear elasticity of any order, with interior penalty for nonconforming symmetric stress approximation. One key point of our method is to introduce some appropriate nonconforming face-bubble spaces based on the local decomposition of discrete symmetric tensors, with which the stability can be easily established. We prove the optimal error estimate for both displacement and stress by adding an interior penalty term. The elements are easy to be implemented thanks to the explicit formulations of its basis functions. Moreover, the methods can be applied to arbitrary simplicial grids for any spatial dimension in a unified fashion. Numerical tests for both 2D and 3D are provided to validate our theoretical results.