Proposal: Proof Assistants
The Proof Assistants site is scheduled to launch into private beta on February 8, 2022.
We want to thank you for your patience, and the time put into the discussion surrounding the site's name and URL and all the suggestions that came up there. After discussing the pros...
@taylor.2317 could you please refrain from making so many edits that do very little to improve the quality of posts. This bumps a lot of old questions to the top of the list without reason. Fixing typos is fine, but some users can find it very annoying having their questions reworded.
Proposal: Proof Assistants
Since we want all proposals to have the best chances of thriving as possible, the Community Team has decided to postpone this proposal's launch into private beta to January 2022, in an attempt to minimize the impact of the upcoming end-of-year holidays in the site's cha...
@NikeDattani Suspended? Has it ever happened in the past? I have never been suspend or even had a disagreement debate with a moderator. However I have seen what SE does to some moderators and employees and don't agree with that.
hi! glad to see this exists. would this be an appropriate stackexchange to ask questions related to using proof assistants for teaching purposes in a math classroom?
The top answer is currently two points ahead. As suggested in the comments, I'll rename the room from "Proof Assistants" to "Tautology" unless anyone objects.
@taylor.2317 Your tag edit for proof-assistants is being presented to me for review. I noted the first time why I rejected it, I will approve this time but don't seek my help if it lands you in hot water.
@wizzwizz4 It's "supposed" to be about theorem provers, but I agree with @AlexNelson that questions about the underpinnings of theorem provers are on topic.
Keep The Activity Up: Try to keep those followers/commiters coming in until the private beta starts. A proposal got auto closed even after getting to 100% commitments.
The division of various SE sites is probably governed by social habits and formation of communities β topics are of a secondary nature, although still important of course. In my opinion it is better to respect the reality of human interaction than to strive for some sort of technically pleasing idealization that will just not work.
@HenryWHHackv3.0b OK. If I were the project manager and I had a choice between fixing some site that has been working and the same for a decade and that would not be noticed if was let alone for a few more months or getting some of the most organized and world class professionals a site they would use up and running, which one do you think I would have taken?
Perhaps a meta post is in order, one question (Announcement) and one answer (Community Wiki); which explains our implementation of highlighting, that we have substituted one available highlighting style with another. Perhaps a second answer for suggestions, which could be edited to be improved or commented on to disagree with - then when the suggestion answer has a part that is perfected that could be implemented (moderator edits the Tag) and the suggestion could be transferred to the
If we want something that highlight.js doesn't natively support, then we'll have to do the development work ourselves, but SE is unlikely to do that. There's some basic packages that SE won't even activate for MathJax, even though they'd involve just adding 1 line to the MathJax call, and even though they'd be useful for several of the sites with high traffic (Math.SE, MathOverflow, Stats.SE, etc.).
@Rob In this end this is what I went for; the request to add custom highlighting was status-declined. Posts tagged lean3 now use haskell highlighting by default. I don't know what the appropriate choice for Coq is, so haven't made one.
This follows on from Syntax highlighting for proof assistants, which establishes that it would be nice to have syntax highlighting, but incorrectly concludes that the ball is not in StackExchange's court.
As mentioned in an answer there, the tool StackExchange uses for highlighting, highlight.js,...
Would a StackExchange employee be able to give an opinion on what level of maturity is required for proofassistants.meta.stackexchange.com/questions/177 to be considered? Pinging @V2Blast since they appear in the editor history of that question
What a shame about rosetta-stone, I don't see how it is any different than what the people over at Code Golf do. It could have been a cool way to get a taste of different proof assistants :(
@AlexNelson Small is relative; it's small compared to its peers. The Scala version of the Lean 3 kernel (Trepplein) has the fewest sloc, it's ~1500. With the Lean 4 features it would probably be ~1650. IMO people who really want maximum assurance will be extracting e.g. Lean proofs and checking them in metamath zero anyway.
@taylor.2317 Out of private beta, it will take 2-4 weeks. Out of public beta, the site needs to wait at least 6 months after it enters public beta, then needs to meet some other requirements too.
@taylor.2317 how long does it usually take for a site to get out of beta (on average)? To be more accurate there is private beta which we are in now and will last around 3 weeks but the SE staff make that decision and will adjust as they see fit. Then there is public beta and that can last from a few months to years. Again the SE staff decides but they do look at these stats here.
It's relevant to the implementation of proof assistants based on type theory, which are dependently-typed languages, where proof checking is type checking.
@wizzwizz4 I would be inclined to say formal proof systems can be discussed here...after all, they're the theoretical underpinnings of theorem provers.
