The paper discusses the current status and future directions of a system for computer-aided analysis of mathematical proofs, consisting of CERES, HLK, and ProofTool. CERES is responsible for cut-elimination, which corresponds to eliminating lemmas in informal proofs, resulting in a direct, lemma-free proof. HLK formalizes mathematical proofs, while ProofTool visualizes them. The system has been applied to three successful cases: the Tape Proof, the Prime Proof, and the Lattice Proof. Future developments include extending the system to second-order logic, improving cut-elimination methods, and enhancing the proof profile to incorporate combinatorial information about proof structure.The paper discusses the current status and future directions of a system for computer-aided analysis of mathematical proofs, consisting of CERES, HLK, and ProofTool. CERES is responsible for cut-elimination, which corresponds to eliminating lemmas in informal proofs, resulting in a direct, lemma-free proof. HLK formalizes mathematical proofs, while ProofTool visualizes them. The system has been applied to three successful cases: the Tape Proof, the Prime Proof, and the Lattice Proof. Future developments include extending the system to second-order logic, improving cut-elimination methods, and enhancing the proof profile to incorporate combinatorial information about proof structure.