The paper presents a system for the computer-aided analysis of mathematical proofs, consisting of three components: HLK, CERES, and ProofTool. HLK formalizes informal proofs into a sequent calculus LKDe, CERES performs cut-elimination to transform proofs into atomic-cut normal form (ACNF), and ProofTool visualizes the results. The system's core is cut-elimination, which removes lemmas from formal proofs, corresponding to direct informal proofs. CERES uses resolution calculus for cut-elimination, extracting Herbrand sequents to summarize the content of ACNF proofs. The system has been applied to three successful cases: the tape proof, the prime proof, and the lattice proof. Future directions include extending the system to second-order logic, handling non-skolemized proofs, supporting superdeduction rules, improving Herbrand sequents, refining resolution methods, and developing an interactive theorem prover. The system aims to enhance the analysis of mathematical proofs, enabling the extraction of direct informal proofs from formal ones.The paper presents a system for the computer-aided analysis of mathematical proofs, consisting of three components: HLK, CERES, and ProofTool. HLK formalizes informal proofs into a sequent calculus LKDe, CERES performs cut-elimination to transform proofs into atomic-cut normal form (ACNF), and ProofTool visualizes the results. The system's core is cut-elimination, which removes lemmas from formal proofs, corresponding to direct informal proofs. CERES uses resolution calculus for cut-elimination, extracting Herbrand sequents to summarize the content of ACNF proofs. The system has been applied to three successful cases: the tape proof, the prime proof, and the lattice proof. Future directions include extending the system to second-order logic, handling non-skolemized proofs, supporting superdeduction rules, improving Herbrand sequents, refining resolution methods, and developing an interactive theorem prover. The system aims to enhance the analysis of mathematical proofs, enabling the extraction of direct informal proofs from formal ones.